Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.7373
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 3878

Launcher Data

LAUNCH ON wulflinc31 THE 2005-09-19 03:19:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2875 boxname=wulflinc31 idbench=531 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a733e9fa1e4e3ac90baf85249f7c3e9a  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-p0282.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-p0282.opb
IDLAUNCH: 2875
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        675080 kB
Buffers:         36940 kB
Cached:         292116 kB
SwapCached:       1016 kB
Active:         107784 kB
Inactive:       224036 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        674828 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5772 kB
Slab:            22068 kB
Committed_AS:    64340 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:39:57 (client local time) WITH STATUS 10 IN 1209.28 SECONDS
stats: 2875 7 1209.28 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 % |

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/22672/stat): 22672 (minisat+_script) R 22671 22672 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846564936 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/22672/statm): 174 3 169 147 0 27 0
[pid=22672] 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=22673
New process pid=22674
New process pid=22675
execve syscall for /bin/sed executable
One traced child (pid=22674) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=22675) exited with status: 0
One traced child (pid=22673) exited with status: 0
New process pid=22676
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-p0282.opb

[startup+10.0032 s]
Raw data (loadavg): 0.91 0.98 0.99 2/58 22676
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8650 0 0 0 931 32 0 0 25 0 1 0 1846564941 38129664 8294 4294967295 134512640 135094434 3221224432 3221222160 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9309 8294 145 145 0 9164 0
[pid=22676] vsize: 37236
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 39360

[startup+20.0052 s]
Raw data (loadavg): 0.93 0.98 0.99 2/58 22676
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8721 0 0 0 1930 33 0 0 25 0 1 0 1846564941 38391808 8365 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9373 8365 145 145 0 9228 0
[pid=22676] vsize: 37492
Current children cumulated CPU time (s) 19.64
Current children cumulated vsize (Kb) 39616

[startup+30.0061 s]
Raw data (loadavg): 0.94 0.98 0.99 2/58 22676
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8795 0 0 0 2928 35 0 0 25 0 1 0 1846564941 38682624 8439 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9444 8439 145 145 0 9299 0
[pid=22676] vsize: 37776
Current children cumulated CPU time (s) 29.64
Current children cumulated vsize (Kb) 39900

[startup+40.0071 s]
Raw data (loadavg): 0.95 0.98 0.99 2/58 22678
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8850 0 0 0 3927 36 0 0 25 0 1 0 1846564941 38903808 8494 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9498 8494 145 145 0 9353 0
[pid=22676] vsize: 37992
Current children cumulated CPU time (s) 39.64
Current children cumulated vsize (Kb) 40116

[startup+50.009 s]
Raw data (loadavg): 0.95 0.98 0.99 2/58 22678
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8932 0 0 0 4925 37 0 0 25 0 1 0 1846564941 39260160 8576 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9585 8576 145 145 0 9440 0
[pid=22676] vsize: 38340
Current children cumulated CPU time (s) 49.63
Current children cumulated vsize (Kb) 40464

[startup+60.0099 s]
Raw data (loadavg): 0.96 0.98 0.99 2/58 22678
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8975 0 0 0 5924 37 0 0 25 0 1 0 1846564941 39428096 8619 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9626 8619 145 145 0 9481 0
[pid=22676] vsize: 38504
Current children cumulated CPU time (s) 59.62
Current children cumulated vsize (Kb) 40628

[startup+70.0119 s]
Raw data (loadavg): 0.97 0.98 0.99 2/58 22678
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9060 0 0 0 6922 39 0 0 25 0 1 0 1846564941 39772160 8704 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9710 8704 145 145 0 9565 0
[pid=22676] vsize: 38840
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 40964

[startup+80.0128 s]
Raw data (loadavg): 0.97 0.98 0.99 2/58 22678
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9193 0 0 0 7920 40 0 0 25 0 1 0 1846564941 40304640 8837 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9840 8837 145 145 0 9695 0
[pid=22676] vsize: 39360
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 41484

[startup+90.0148 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 22678
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9257 0 0 0 8918 41 0 0 25 0 1 0 1846564941 40566784 8901 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9904 8901 145 145 0 9759 0
[pid=22676] vsize: 39616
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 41740

[startup+100.016 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 22680
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9319 0 0 0 9917 42 0 0 25 0 1 0 1846564941 40808448 8963 4294967295 134512640 135094434 3221224432 3221222992 134550329 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 9963 8963 145 145 0 9818 0
[pid=22676] vsize: 39852
Current children cumulated CPU time (s) 99.6
Current children cumulated vsize (Kb) 41976

[startup+110.017 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 22680
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9371 0 0 0 10916 42 0 0 25 0 1 0 1846564941 41070592 9015 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 10027 9015 145 145 0 9882 0
[pid=22676] vsize: 40108
Current children cumulated CPU time (s) 109.59
Current children cumulated vsize (Kb) 42232

[startup+120.019 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 22680
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9451 0 0 0 11914 44 0 0 25 0 1 0 1846564941 41385984 9095 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 10104 9095 145 145 0 9959 0
[pid=22676] vsize: 40416
Current children cumulated CPU time (s) 119.59
Current children cumulated vsize (Kb) 42540

[startup+130.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22680
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9537 0 0 0 12912 45 0 0 25 0 1 0 1846564941 41734144 9181 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22676/statm): 10189 9181 145 145 0 10044 0
[pid=22676] vsize: 40756
Current children cumulated CPU time (s) 129.58
Current children cumulated vsize (Kb) 42880

[startup+140.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22680
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9614 0 0 0 13911 45 0 0 25 0 1 0 1846564941 42049536 9258 4294967295 134512640 135094434 3221224432 3221222212 134676464 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10266 9258 145 145 0 10121 0
[pid=22676] vsize: 41064
Current children cumulated CPU time (s) 139.57
Current children cumulated vsize (Kb) 43188

[startup+150.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22680
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9651 0 0 0 14911 45 0 0 25 0 1 0 1846564941 42172416 9295 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10296 9295 145 145 0 10151 0
[pid=22676] vsize: 41184
Current children cumulated CPU time (s) 149.57
Current children cumulated vsize (Kb) 43308

[startup+160.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22682
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9751 0 0 0 15909 47 0 0 25 0 1 0 1846564941 42561536 9395 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10391 9395 145 145 0 10246 0
[pid=22676] vsize: 41564
Current children cumulated CPU time (s) 159.57
Current children cumulated vsize (Kb) 43688

[startup+170.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22682
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9880 0 0 0 16907 48 0 0 25 0 1 0 1846564941 43085824 9524 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10519 9524 145 145 0 10374 0
[pid=22676] vsize: 42076
Current children cumulated CPU time (s) 169.56
Current children cumulated vsize (Kb) 44200

[startup+180.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22682
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9954 0 0 0 17906 48 0 0 25 0 1 0 1846564941 43384832 9598 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10592 9598 145 145 0 10447 0
[pid=22676] vsize: 42368
Current children cumulated CPU time (s) 179.55
Current children cumulated vsize (Kb) 44492

[startup+190.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22682
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10080 0 0 0 18904 49 0 0 25 0 1 0 1846564941 43888640 9724 4294967295 134512640 135094434 3221224432 3221221312 134519159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10715 9724 145 145 0 10570 0
[pid=22676] vsize: 42860
Current children cumulated CPU time (s) 189.54
Current children cumulated vsize (Kb) 44984

[startup+200.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22682
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10149 0 0 0 19903 50 0 0 25 0 1 0 1846564941 44298240 9793 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10815 9793 145 145 0 10670 0
[pid=22676] vsize: 43260
Current children cumulated CPU time (s) 199.54
Current children cumulated vsize (Kb) 45384

[startup+210.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22682
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10213 0 0 0 20902 50 0 0 25 0 1 0 1846564941 44556288 9857 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10878 9857 145 145 0 10733 0
[pid=22676] vsize: 43512
Current children cumulated CPU time (s) 209.53
Current children cumulated vsize (Kb) 45636

[startup+220.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22684
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10290 0 0 0 21901 51 0 0 25 0 1 0 1846564941 44879872 9934 4294967295 134512640 135094434 3221224432 3221223104 134555945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 10957 9934 145 145 0 10812 0
[pid=22676] vsize: 43828
Current children cumulated CPU time (s) 219.53
Current children cumulated vsize (Kb) 45952

[startup+230.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22684
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10365 0 0 0 22901 51 0 0 25 0 1 0 1846564941 45277184 10009 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11054 10009 145 145 0 10909 0
[pid=22676] vsize: 44216
Current children cumulated CPU time (s) 229.53
Current children cumulated vsize (Kb) 46340

[startup+240.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22684
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) T 22672 22672 9102 0 -1 0 10406 0 0 0 23900 51 0 0 25 0 1 0 1846564941 45441024 10050 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11094 10050 145 145 0 10949 0
[pid=22676] vsize: 44376
Current children cumulated CPU time (s) 239.52
Current children cumulated vsize (Kb) 46500

[startup+250.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22684
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10470 0 0 0 24899 52 0 0 25 0 1 0 1846564941 45699072 10114 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11157 10114 145 145 0 11012 0
[pid=22676] vsize: 44628
Current children cumulated CPU time (s) 249.52
Current children cumulated vsize (Kb) 46752

[startup+260.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22684
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10566 0 0 0 25897 53 0 0 25 0 1 0 1846564941 46092288 10210 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11253 10210 145 145 0 11108 0
[pid=22676] vsize: 45012
Current children cumulated CPU time (s) 259.51
Current children cumulated vsize (Kb) 47136

[startup+270.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22684
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10685 0 0 0 26895 53 0 0 25 0 1 0 1846564941 46567424 10329 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11369 10329 145 145 0 11224 0
[pid=22676] vsize: 45476
Current children cumulated CPU time (s) 269.49
Current children cumulated vsize (Kb) 47600

[startup+280.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22686
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10760 0 0 0 27893 54 0 0 25 0 1 0 1846564941 46870528 10404 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11443 10404 145 145 0 11298 0
[pid=22676] vsize: 45772
Current children cumulated CPU time (s) 279.48
Current children cumulated vsize (Kb) 47896

[startup+290.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22686
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10851 0 0 0 28893 55 0 0 25 0 1 0 1846564941 47243264 10495 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11534 10495 145 145 0 11389 0
[pid=22676] vsize: 46136
Current children cumulated CPU time (s) 289.49
Current children cumulated vsize (Kb) 48260

[startup+300.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22686
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10934 0 0 0 29892 55 0 0 25 0 1 0 1846564941 47579136 10578 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11616 10578 145 145 0 11471 0
[pid=22676] vsize: 46464
Current children cumulated CPU time (s) 299.48
Current children cumulated vsize (Kb) 48588

[startup+310.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22686
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11015 0 0 0 30891 56 0 0 25 0 1 0 1846564941 47906816 10659 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11696 10659 145 145 0 11551 0
[pid=22676] vsize: 46784
Current children cumulated CPU time (s) 309.48
Current children cumulated vsize (Kb) 48908

[startup+320.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22686
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11129 0 0 0 31888 57 0 0 25 0 1 0 1846564941 48369664 10773 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11809 10773 145 145 0 11664 0
[pid=22676] vsize: 47236
Current children cumulated CPU time (s) 319.46
Current children cumulated vsize (Kb) 49360

[startup+330.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22686
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11205 0 0 0 32888 57 0 0 25 0 1 0 1846564941 48676864 10849 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11884 10849 145 145 0 11739 0
[pid=22676] vsize: 47536
Current children cumulated CPU time (s) 329.46
Current children cumulated vsize (Kb) 49660

[startup+340.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22688
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11297 0 0 0 33886 58 0 0 25 0 1 0 1846564941 49053696 10941 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 11976 10941 145 145 0 11831 0
[pid=22676] vsize: 47904
Current children cumulated CPU time (s) 339.45
Current children cumulated vsize (Kb) 50028

[startup+350.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22688
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11360 0 0 0 34885 59 0 0 25 0 1 0 1846564941 49307648 11004 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12038 11004 145 145 0 11893 0
[pid=22676] vsize: 48152
Current children cumulated CPU time (s) 349.45
Current children cumulated vsize (Kb) 50276

[startup+360.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22688
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11425 0 0 0 35885 59 0 0 25 0 1 0 1846564941 49569792 11069 4294967295 134512640 135094434 3221224432 3221221808 134600283 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12102 11069 145 145 0 11957 0
[pid=22676] vsize: 48408
Current children cumulated CPU time (s) 359.45
Current children cumulated vsize (Kb) 50532

[startup+370.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22688
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11445 0 0 0 36884 59 0 0 25 0 1 0 1846564941 49647616 11089 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12121 11089 145 145 0 11976 0
[pid=22676] vsize: 48484
Current children cumulated CPU time (s) 369.44
Current children cumulated vsize (Kb) 50608

[startup+380.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22688
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11557 0 0 0 37883 60 0 0 25 0 1 0 1846564941 50098176 11201 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12231 11201 145 145 0 12086 0
[pid=22676] vsize: 48924
Current children cumulated CPU time (s) 379.44
Current children cumulated vsize (Kb) 51048

[startup+390.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22688
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11639 0 0 0 38882 60 0 0 25 0 1 0 1846564941 50429952 11283 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12312 11283 145 145 0 12167 0
[pid=22676] vsize: 49248
Current children cumulated CPU time (s) 389.43
Current children cumulated vsize (Kb) 51372

[startup+400.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22690
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11764 0 0 0 39880 61 0 0 25 0 1 0 1846564941 50937856 11408 4294967295 134512640 135094434 3221224432 3221221552 134676999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12436 11408 145 145 0 12291 0
[pid=22676] vsize: 49744
Current children cumulated CPU time (s) 399.42
Current children cumulated vsize (Kb) 51868

[startup+410.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22690
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11778 0 0 0 40880 61 0 0 25 0 1 0 1846564941 50991104 11422 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12449 11422 145 145 0 12304 0
[pid=22676] vsize: 49796
Current children cumulated CPU time (s) 409.42
Current children cumulated vsize (Kb) 51920

[startup+420.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22690
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11855 0 0 0 41878 62 0 0 25 0 1 0 1846564941 51302400 11499 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12525 11499 145 145 0 12380 0
[pid=22676] vsize: 50100
Current children cumulated CPU time (s) 419.41
Current children cumulated vsize (Kb) 52224

[startup+430.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22690
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11940 0 0 0 42877 63 0 0 25 0 1 0 1846564941 51646464 11584 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12609 11584 145 145 0 12464 0
[pid=22676] vsize: 50436
Current children cumulated CPU time (s) 429.41
Current children cumulated vsize (Kb) 52560

[startup+440.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22690
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12009 0 0 0 43876 64 0 0 25 0 1 0 1846564941 51929088 11653 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12678 11653 145 145 0 12533 0
[pid=22676] vsize: 50712
Current children cumulated CPU time (s) 439.41
Current children cumulated vsize (Kb) 52836

[startup+450.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22690
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12051 0 0 0 44875 65 0 0 25 0 1 0 1846564941 52097024 11695 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12719 11695 145 145 0 12574 0
[pid=22676] vsize: 50876
Current children cumulated CPU time (s) 449.41
Current children cumulated vsize (Kb) 53000

[startup+460.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22692
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12096 0 0 0 45873 66 0 0 25 0 1 0 1846564941 52277248 11740 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12763 11740 145 145 0 12618 0
[pid=22676] vsize: 51052
Current children cumulated CPU time (s) 459.4
Current children cumulated vsize (Kb) 53176

[startup+470.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22692
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12171 0 0 0 46872 67 0 0 25 0 1 0 1846564941 52580352 11815 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12837 11815 145 145 0 12692 0
[pid=22676] vsize: 51348
Current children cumulated CPU time (s) 469.4
Current children cumulated vsize (Kb) 53472

[startup+480.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22692
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12252 0 0 0 47871 68 0 0 25 0 1 0 1846564941 52912128 11896 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12918 11896 145 145 0 12773 0
[pid=22676] vsize: 51672
Current children cumulated CPU time (s) 479.4
Current children cumulated vsize (Kb) 53796

[startup+490.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22692
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12331 0 0 0 48870 69 0 0 25 0 1 0 1846564941 53231616 11975 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 12996 11975 145 145 0 12851 0
[pid=22676] vsize: 51984
Current children cumulated CPU time (s) 489.4
Current children cumulated vsize (Kb) 54108

[startup+500.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22692
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12405 0 0 0 49869 70 0 0 25 0 1 0 1846564941 53530624 12049 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13069 12049 145 145 0 12924 0
[pid=22676] vsize: 52276
Current children cumulated CPU time (s) 499.4
Current children cumulated vsize (Kb) 54400

[startup+510.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22692
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12515 0 0 0 50867 71 0 0 25 0 1 0 1846564941 53977088 12159 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13178 12159 145 145 0 13033 0
[pid=22676] vsize: 52712
Current children cumulated CPU time (s) 509.39
Current children cumulated vsize (Kb) 54836

[startup+520.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22694
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12572 0 0 0 51866 71 0 0 25 0 1 0 1846564941 54206464 12216 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13234 12216 145 145 0 13089 0
[pid=22676] vsize: 52936
Current children cumulated CPU time (s) 519.38
Current children cumulated vsize (Kb) 55060

[startup+530.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22694
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12621 0 0 0 52866 71 0 0 25 0 1 0 1846564941 54665216 12265 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13346 12265 145 145 0 13201 0
[pid=22676] vsize: 53384
Current children cumulated CPU time (s) 529.38
Current children cumulated vsize (Kb) 55508

[startup+540.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22694
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12672 0 0 0 53865 72 0 0 25 0 1 0 1846564941 54870016 12316 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13396 12316 145 145 0 13251 0
[pid=22676] vsize: 53584
Current children cumulated CPU time (s) 539.38
Current children cumulated vsize (Kb) 55708

[startup+550.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22694
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12717 0 0 0 54865 72 0 0 25 0 1 0 1846564941 55054336 12361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13441 12361 145 145 0 13296 0
[pid=22676] vsize: 53764
Current children cumulated CPU time (s) 549.38
Current children cumulated vsize (Kb) 55888

[startup+560.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22694
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12791 0 0 0 55864 72 0 0 25 0 1 0 1846564941 55353344 12435 4294967295 134512640 135094434 3221224432 3221222220 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13514 12435 145 145 0 13369 0
[pid=22676] vsize: 54056
Current children cumulated CPU time (s) 559.37
Current children cumulated vsize (Kb) 56180

[startup+570.068 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22694
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12809 0 0 0 56864 73 0 0 25 0 1 0 1846564941 55422976 12453 4294967295 134512640 135094434 3221224432 3221223056 134557724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13531 12453 145 145 0 13386 0
[pid=22676] vsize: 54124
Current children cumulated CPU time (s) 569.38
Current children cumulated vsize (Kb) 56248

[startup+580.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22696
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12874 0 0 0 57863 73 0 0 25 0 1 0 1846564941 55685120 12518 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13595 12518 145 145 0 13450 0
[pid=22676] vsize: 54380
Current children cumulated CPU time (s) 579.37
Current children cumulated vsize (Kb) 56504

[startup+590.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22696
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12995 0 0 0 58861 74 0 0 25 0 1 0 1846564941 56168448 12639 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13713 12639 145 145 0 13568 0
[pid=22676] vsize: 54852
Current children cumulated CPU time (s) 589.36
Current children cumulated vsize (Kb) 56976

[startup+600.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22696
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13041 0 0 0 59860 75 0 0 25 0 1 0 1846564941 56356864 12685 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13759 12685 145 145 0 13614 0
[pid=22676] vsize: 55036
Current children cumulated CPU time (s) 599.36
Current children cumulated vsize (Kb) 57160

[startup+610.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22696
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13139 0 0 0 60858 75 0 0 25 0 1 0 1846564941 56745984 12783 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13854 12783 145 145 0 13709 0
[pid=22676] vsize: 55416
Current children cumulated CPU time (s) 609.34
Current children cumulated vsize (Kb) 57540

[startup+620.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22696
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13196 0 0 0 61858 75 0 0 25 0 1 0 1846564941 56983552 12840 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13912 12840 145 145 0 13767 0
[pid=22676] vsize: 55648
Current children cumulated CPU time (s) 619.34
Current children cumulated vsize (Kb) 57772

[startup+630.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22696
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13269 0 0 0 62857 76 0 0 25 0 1 0 1846564941 57278464 12913 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 13984 12913 145 145 0 13839 0
[pid=22676] vsize: 55936
Current children cumulated CPU time (s) 629.34
Current children cumulated vsize (Kb) 58060

[startup+640.074 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22698
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13356 0 0 0 63855 77 0 0 25 0 1 0 1846564941 57626624 13000 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14069 13000 145 145 0 13924 0
[pid=22676] vsize: 56276
Current children cumulated CPU time (s) 639.33
Current children cumulated vsize (Kb) 58400

[startup+650.075 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22698
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13415 0 0 0 64855 77 0 0 25 0 1 0 1846564941 57864192 13059 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14127 13059 145 145 0 13982 0
[pid=22676] vsize: 56508
Current children cumulated CPU time (s) 649.33
Current children cumulated vsize (Kb) 58632

[startup+660.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22698
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13486 0 0 0 65854 78 0 0 25 0 1 0 1846564941 58155008 13130 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14198 13130 145 145 0 14053 0
[pid=22676] vsize: 56792
Current children cumulated CPU time (s) 659.33
Current children cumulated vsize (Kb) 58916

[startup+670.077 s]
Raw data (loadavg): 0.99 0.98 0.99 1/58 22698
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) T 22672 22672 9102 0 -1 0 13509 0 0 0 66854 78 0 0 25 0 1 0 1846564941 58245120 13153 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14220 13153 145 145 0 14075 0
[pid=22676] vsize: 56880
Current children cumulated CPU time (s) 669.33
Current children cumulated vsize (Kb) 59004

[startup+680.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22698
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13551 0 0 0 67853 79 0 0 25 0 1 0 1846564941 58413056 13195 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14261 13195 145 145 0 14116 0
[pid=22676] vsize: 57044
Current children cumulated CPU time (s) 679.33
Current children cumulated vsize (Kb) 59168

[startup+690.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22698
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13597 0 0 0 68853 79 0 0 25 0 1 0 1846564941 58597376 13241 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14306 13241 145 145 0 14161 0
[pid=22676] vsize: 57224
Current children cumulated CPU time (s) 689.33
Current children cumulated vsize (Kb) 59348

[startup+700.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22700
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13648 0 0 0 69851 80 0 0 25 0 1 0 1846564941 58810368 13292 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14358 13292 145 145 0 14213 0
[pid=22676] vsize: 57432
Current children cumulated CPU time (s) 699.32
Current children cumulated vsize (Kb) 59556

[startup+710.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22700
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13742 0 0 0 70850 80 0 0 25 0 1 0 1846564941 59191296 13386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14451 13386 145 145 0 14306 0
[pid=22676] vsize: 57804
Current children cumulated CPU time (s) 709.31
Current children cumulated vsize (Kb) 59928

[startup+720.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22700
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13808 0 0 0 71849 81 0 0 25 0 1 0 1846564941 59457536 13452 4294967295 134512640 135094434 3221224432 3221223104 134556394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14516 13452 145 145 0 14371 0
[pid=22676] vsize: 58064
Current children cumulated CPU time (s) 719.31
Current children cumulated vsize (Kb) 60188

[startup+730.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22700
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13871 0 0 0 72848 81 0 0 25 0 1 0 1846564941 59715584 13515 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14579 13515 145 145 0 14434 0
[pid=22676] vsize: 58316
Current children cumulated CPU time (s) 729.3
Current children cumulated vsize (Kb) 60440

[startup+740.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22700
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13948 0 0 0 73846 82 0 0 25 0 1 0 1846564941 60026880 13592 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14655 13592 145 145 0 14510 0
[pid=22676] vsize: 58620
Current children cumulated CPU time (s) 739.29
Current children cumulated vsize (Kb) 60744

[startup+750.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22700
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14030 0 0 0 74845 83 0 0 25 0 1 0 1846564941 60362752 13674 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14737 13674 145 145 0 14592 0
[pid=22676] vsize: 58948
Current children cumulated CPU time (s) 749.29
Current children cumulated vsize (Kb) 61072

[startup+760.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22702
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14114 0 0 0 75844 83 0 0 25 0 1 0 1846564941 60698624 13758 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14819 13758 145 145 0 14674 0
[pid=22676] vsize: 59276
Current children cumulated CPU time (s) 759.28
Current children cumulated vsize (Kb) 61400

[startup+770.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22702
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14212 0 0 0 76843 84 0 0 25 0 1 0 1846564941 61095936 13856 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14916 13856 145 145 0 14771 0
[pid=22676] vsize: 59664
Current children cumulated CPU time (s) 769.28
Current children cumulated vsize (Kb) 61788

[startup+780.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22702
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14283 0 0 0 77842 84 0 0 25 0 1 0 1846564941 61386752 13927 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 14987 13927 145 145 0 14842 0
[pid=22676] vsize: 59948
Current children cumulated CPU time (s) 779.27
Current children cumulated vsize (Kb) 62072

[startup+790.089 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22702
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14426 0 0 0 78840 86 0 0 25 0 1 0 1846564941 61968384 14070 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15129 14070 145 145 0 14984 0
[pid=22676] vsize: 60516
Current children cumulated CPU time (s) 789.27
Current children cumulated vsize (Kb) 62640

[startup+800.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22702
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14578 0 0 0 79838 87 0 0 25 0 1 0 1846564941 62586880 14222 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15280 14222 145 145 0 15135 0
[pid=22676] vsize: 61120
Current children cumulated CPU time (s) 799.26
Current children cumulated vsize (Kb) 63244

[startup+810.091 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22702
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14650 0 0 0 80837 87 0 0 25 0 1 0 1846564941 62881792 14294 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15352 14294 145 145 0 15207 0
[pid=22676] vsize: 61408
Current children cumulated CPU time (s) 809.25
Current children cumulated vsize (Kb) 63532

[startup+820.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22704
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14782 0 0 0 81835 88 0 0 25 0 1 0 1846564941 63426560 14426 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15485 14426 145 145 0 15340 0
[pid=22676] vsize: 61940
Current children cumulated CPU time (s) 819.24
Current children cumulated vsize (Kb) 64064

[startup+830.093 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22704
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14881 0 0 0 82834 88 0 0 25 0 1 0 1846564941 63840256 14525 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15586 14525 145 145 0 15441 0
[pid=22676] vsize: 62344
Current children cumulated CPU time (s) 829.23
Current children cumulated vsize (Kb) 64468

[startup+840.095 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22704
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15081 0 0 0 83831 90 0 0 25 0 1 0 1846564941 64651264 14725 4294967295 134512640 135094434 3221224432 3221221808 134600225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15784 14725 145 145 0 15639 0
[pid=22676] vsize: 63136
Current children cumulated CPU time (s) 839.22
Current children cumulated vsize (Kb) 65260

[startup+850.096 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22704
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15098 0 0 0 84831 90 0 0 25 0 1 0 1846564941 64716800 14742 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15800 14742 145 145 0 15655 0
[pid=22676] vsize: 63200
Current children cumulated CPU time (s) 849.22
Current children cumulated vsize (Kb) 65324

[startup+860.096 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22704
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15175 0 0 0 85830 91 0 0 25 0 1 0 1846564941 65048576 14819 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15881 14819 145 145 0 15736 0
[pid=22676] vsize: 63524
Current children cumulated CPU time (s) 859.22
Current children cumulated vsize (Kb) 65648

[startup+870.097 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22704
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15237 0 0 0 86828 91 0 0 25 0 1 0 1846564941 65294336 14881 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 15941 14881 145 145 0 15796 0
[pid=22676] vsize: 63764
Current children cumulated CPU time (s) 869.2
Current children cumulated vsize (Kb) 65888

[startup+880.098 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22706
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15306 0 0 0 87828 92 0 0 25 0 1 0 1846564941 65576960 14950 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16010 14950 145 145 0 15865 0
[pid=22676] vsize: 64040
Current children cumulated CPU time (s) 879.21
Current children cumulated vsize (Kb) 66164

[startup+890.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22706
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15347 0 0 0 88828 92 0 0 25 0 1 0 1846564941 65740800 14991 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16050 14991 145 145 0 15905 0
[pid=22676] vsize: 64200
Current children cumulated CPU time (s) 889.21
Current children cumulated vsize (Kb) 66324

[startup+900.101 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22706
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15414 0 0 0 89827 92 0 0 25 0 1 0 1846564941 66019328 15058 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16118 15058 145 145 0 15973 0
[pid=22676] vsize: 64472
Current children cumulated CPU time (s) 899.2
Current children cumulated vsize (Kb) 66596

[startup+910.101 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22706
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15465 0 0 0 90827 92 0 0 25 0 1 0 1846564941 66232320 15109 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16170 15109 145 145 0 16025 0
[pid=22676] vsize: 64680
Current children cumulated CPU time (s) 909.2
Current children cumulated vsize (Kb) 66804

[startup+920.102 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22706
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15552 0 0 0 91826 93 0 0 25 0 1 0 1846564941 66584576 15196 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16256 15196 145 145 0 16111 0
[pid=22676] vsize: 65024
Current children cumulated CPU time (s) 919.2
Current children cumulated vsize (Kb) 67148

[startup+930.103 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22706
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15639 0 0 0 92824 93 0 0 25 0 1 0 1846564941 66940928 15283 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16343 15283 145 145 0 16198 0
[pid=22676] vsize: 65372
Current children cumulated CPU time (s) 929.18
Current children cumulated vsize (Kb) 67496

[startup+940.104 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22708
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15731 0 0 0 93823 95 0 0 25 0 1 0 1846564941 67309568 15375 4294967295 134512640 135094434 3221224432 3221221248 134600704 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15375 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 939.19
Current children cumulated vsize (Kb) 67856

[startup+950.105 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22708
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15731 0 0 0 94823 95 0 0 25 0 1 0 1846564941 67309568 15375 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15375 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 949.19
Current children cumulated vsize (Kb) 67856

[startup+960.106 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22708
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15731 0 0 0 95823 95 0 0 25 0 1 0 1846564941 67309568 15375 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15375 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 959.19
Current children cumulated vsize (Kb) 67856

[startup+970.107 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22708
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 96823 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221222912 134781309 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 969.19
Current children cumulated vsize (Kb) 67856

[startup+980.108 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22708
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 97823 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 979.19
Current children cumulated vsize (Kb) 67856

[startup+990.109 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22708
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 98823 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221221904 134677069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 989.19
Current children cumulated vsize (Kb) 67856

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22710
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 99824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 999.2
Current children cumulated vsize (Kb) 67856

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22710
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 100824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1009.2
Current children cumulated vsize (Kb) 67856

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22710
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 101824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1019.2
Current children cumulated vsize (Kb) 67856

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22710
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 102824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1029.2
Current children cumulated vsize (Kb) 67856

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22710
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 103824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1039.2
Current children cumulated vsize (Kb) 67856

[startup+1050.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22710
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 104824 96 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1049.21
Current children cumulated vsize (Kb) 67856

[startup+1060.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22712
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 105823 97 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1059.21
Current children cumulated vsize (Kb) 67856

[startup+1070.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22712
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 106823 97 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1069.21
Current children cumulated vsize (Kb) 67856

[startup+1080.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22712
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 107823 98 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1079.22
Current children cumulated vsize (Kb) 67856

[startup+1090.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22712
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 108823 98 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1089.22
Current children cumulated vsize (Kb) 67856

[startup+1100.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22712
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 109823 98 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223220 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1099.22
Current children cumulated vsize (Kb) 67856

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22712
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 110823 98 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1109.22
Current children cumulated vsize (Kb) 67856

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22714
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 111823 98 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1119.22
Current children cumulated vsize (Kb) 67856

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22714
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 112823 98 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1129.22
Current children cumulated vsize (Kb) 67856

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22714
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 113823 99 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1139.23
Current children cumulated vsize (Kb) 67856

[startup+1150.13 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22714
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 114823 99 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1149.23
Current children cumulated vsize (Kb) 67856

[startup+1160.13 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22714
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 115823 99 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1159.23
Current children cumulated vsize (Kb) 67856

[startup+1170.13 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22714
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 116823 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1169.23
Current children cumulated vsize (Kb) 67856

[startup+1180.13 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22716
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 117824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1179.24
Current children cumulated vsize (Kb) 67856

[startup+1190.13 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22716
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 118824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1189.24
Current children cumulated vsize (Kb) 67856

[startup+1200.13 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22716
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 119824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1199.24
Current children cumulated vsize (Kb) 67856

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22716
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 120824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1209.24
Current children cumulated vsize (Kb) 67856



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22716
Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22672/statm): 531 226 485 147 0 384 0
[pid=22672] vsize: 2124
Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 120824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0
[pid=22676] vsize: 65732
Current children cumulated CPU time (s) 1209.24
Current children cumulated vsize (Kb) 67856

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

Child status: 10
Real time (s): 1210.17
CPU time (s): 1209.28
CPU user time (s): 1208.25
CPU system time (s): 1.02984
CPU usage (%): 99.9266
Max. virtual memory (cumulated for all children) (Kb): 67856

Verifier Data

ERROR: no interpretation found !