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/miplib2003/normalized-mps-v2-20-10-markshare1.opb
MD5SUM10386fd19d9976c249ce2be861b38a70
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 36864
Optimality of the best value was proved NO
Number of terms in the objective function 180
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 6442450938
Number of bits of the sum of numbers in the objective function 33
Biggest number in a constraint 536870912
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 6442450938
Number of bits of the biggest sum of numbers33
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.29
Number of variables230
Total number of constraints56
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)50
Number of constraints which are nor clauses,nor cardinality constraints6
Minimum length of a constraint1
Maximum length of a constraint80

Trace number 3911

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        885744 kB
Buffers:         36668 kB
Cached:          83336 kB
SwapCached:        832 kB
Active:          71144 kB
Inactive:        51556 kB
HighTotal:      131008 kB
HighFree:        44324 kB
LowTotal:       903652 kB
LowFree:        841420 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20596 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 04:01:13 (client local time) WITH STATUS 10 IN 1209.92 SECONDS
stats: 2916 7 1209.92 10

Solver Data

c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> Adder-cost: 304   maxlim: 3240959   bits: 23/22
c ---[   8]---> Adder-cost: 314   maxlim: 3453951   bits: 23/22
c ---[   6]---> Adder-cost: 348   maxlim: 3482623   bits: 23/22
c ---[   4]---> Adder-cost: 318   maxlim: 3294207   bits: 23/22
c ---[   2]---> Adder-cost: 312   maxlim: 3286015   bits: 23/22
c ---[   0]---> Adder-cost: 314   maxlim: 3289087   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12820    45524 |    4273       0        0     nan |  0.000 % |
c |       100 |   12820    45524 |    4700     100      594     5.9 | 14.261 % |
c ==============================================================================
c Found solution: 4615168
c ---[   0]---> Sorter-cost:  850     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       141 |   14814    50194 |    4938     141     1027     7.3 | 14.261 % |
c |       241 |   14814    50194 |    5431     241    12192    50.6 | 10.969 % |
c |       393 |   14814    50194 |    5974     393    26032    66.2 | 10.969 % |
c |       618 |   14814    50194 |    6572     618    37060    60.0 | 10.969 % |
c |       955 |   14814    50194 |    7229     955    69049    72.3 | 10.969 % |
c ==============================================================================
c Found solution: 4444160
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1006 |   14929    50490 |    4976    1006    70987    70.6 | 10.969 % |
c |      1107 |   14929    50490 |    5473    1107    85930    77.6 | 10.770 % |
c ==============================================================================
c Found solution: 4152320
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1139 |   14941    50532 |    4980    1139    86375    75.8 | 10.770 % |
c |      1240 |   14941    50532 |    5478    1240    94355    76.1 | 10.771 % |
c |      1390 |   14941    50532 |    6025    1390   106104    76.3 | 10.771 % |
c ==============================================================================
c Found solution: 3231744
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1590 |   14951    50556 |    4983    1590   117597    74.0 | 10.771 % |
c |      1691 |   14951    50556 |    5481    1691   130635    77.3 | 10.786 % |
c |      1841 |   14951    50556 |    6029    1841   142489    77.4 | 10.786 % |
c |      2067 |   14943    50530 |    6632    2066   165570    80.1 | 10.819 % |
c |      2404 |   14943    50530 |    7295    2403   186034    77.4 | 10.819 % |
c |      2910 |   14943    50530 |    8025    2909   234223    80.5 | 10.819 % |
c |      3669 |   14935    50504 |    8827    3667   297711    81.2 | 10.852 % |
c |      4810 |   14919    50452 |    9710    4806   397534    82.7 | 10.917 % |
c |      6518 |   14919    50452 |   10681    6514   543132    83.4 | 10.917 % |
c |      9081 |   14919    50452 |   11749    9077   695094    76.6 | 10.917 % |
c ==============================================================================
c Found solution: 3212288
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11955 |   14931    50479 |    4977   11951   922500    77.2 | 10.917 % |
c |     12056 |   14931    50479 |    5474    3089   184035    59.6 | 10.932 % |
c |     12207 |   14931    50479 |    6022    3240   193746    59.8 | 10.932 % |
c |     12433 |   14931    50479 |    6624    3466   204232    58.9 | 10.932 % |
c |     12770 |   14931    50479 |    7286    3803   246752    64.9 | 10.932 % |
c |     13278 |   14923    50453 |    8015    4310   287955    66.8 | 10.965 % |
c |     14042 |   14923    50453 |    8817    5074   357875    70.5 | 10.965 % |
c |     15182 |   14923    50453 |    9698    6214   454785    73.2 | 10.965 % |
c |     16891 |   14923    50453 |   10668    7923   596983    75.3 | 10.965 % |
c |     19453 |   14915    50427 |   11735   10484   806542    76.9 | 10.998 % |
c |     23299 |   14907    50401 |   12909    7910   531028    67.1 | 11.031 % |
c |     29065 |   14891    50349 |   14199   13674  1005814    73.6 | 11.097 % |
c |     37715 |   14884    50334 |   15619   14705  1118217    76.0 | 11.162 % |
c ==============================================================================
c Found solution: 3169280
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45485 |   14886    50339 |    4962   14152  1130949    79.9 | 11.162 % |
c |     45586 |   14886    50339 |    5458    3639   207343    57.0 | 11.253 % |
c |     45736 |   14886    50339 |    6004    3789   218603    57.7 | 11.253 % |
c |     45961 |   14886    50339 |    6604    4014   238535    59.4 | 11.253 % |
c |     46300 |   14886    50339 |    7264    4353   272968    62.7 | 11.253 % |
c |     46807 |   14878    50313 |    7991    4859   321893    66.2 | 11.286 % |
c |     47567 |   14878    50313 |    8790    5619   395734    70.4 | 11.286 % |
c |     48706 |   14878    50313 |    9669    6758   514295    76.1 | 11.286 % |
c |     50414 |   14878    50313 |   10636    8466   674245    79.6 | 11.286 % |
c |     52979 |   14878    50313 |   11700   11031   894758    81.1 | 11.286 % |
c |     56823 |   14878    50313 |   12870    8476   585487    69.1 | 11.286 % |
c |     62589 |   14878    50313 |   14157    7246   470267    64.9 | 11.286 % |
c |     71238 |   14878    50313 |   15572    8340   484689    58.1 | 11.286 % |
c ==============================================================================
c Found solution: 3042304
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81326 |   14886    50332 |    4962   10127   656025    64.8 | 11.286 % |
c |     81428 |   14886    50332 |    5458    5166   279097    54.0 | 11.300 % |
c |     81579 |   14886    50332 |    6004    5317   292474    55.0 | 11.300 % |
c |     81804 |   14886    50332 |    6604    5542   307973    55.6 | 11.300 % |
c |     82141 |   14886    50332 |    7264    5879   344300    58.6 | 11.300 % |
c |     82647 |   14886    50332 |    7991    6385   389480    61.0 | 11.300 % |
c |     83406 |   14886    50332 |    8790    7144   439505    61.5 | 11.300 % |
c |     84547 |   14886    50332 |    9669    8285   529161    63.9 | 11.300 % |
c |     86259 |   14886    50332 |   10636    9997   662102    66.2 | 11.300 % |
c |     88822 |   14886    50332 |   11700    6767   420905    62.2 | 11.300 % |
c |     92668 |   14886    50332 |   12870   10613   744951    70.2 | 11.300 % |
c |     98434 |   14886    50332 |   14157    9409   652200    69.3 | 11.300 % |
c |    107085 |   14886    50332 |   15572   10478   637247    60.8 | 11.300 % |
c ==============================================================================
c Found solution: 3005440
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111385 |   14888    50336 |    4962   14777   921886    62.4 | 11.300 % |
c |    111486 |   14888    50336 |    5458    3796   173019    45.6 | 11.344 % |
c |    111636 |   14888    50336 |    6004    3946   179318    45.4 | 11.344 % |
c |    111861 |   14888    50336 |    6604    4171   192217    46.1 | 11.344 % |
c |    112199 |   14880    50310 |    7264    4508   220479    48.9 | 11.376 % |
c |    112705 |   14880    50310 |    7991    5014   263662    52.6 | 11.376 % |
c |    113465 |   14880    50310 |    8790    5774   310667    53.8 | 11.376 % |
c |    114604 |   14880    50310 |    9669    6913   409090    59.2 | 11.376 % |
c |    116313 |   14872    50284 |   10636    8621   542723    63.0 | 11.409 % |
c |    118875 |   14864    50258 |   11700   11182   716184    64.0 | 11.442 % |
c |    122719 |   14864    50258 |   12870    8765   560433    63.9 | 11.442 % |
c ==============================================================================
c Found solution: 2816000
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    124383 |   14877    50289 |    4959   10429   657968    63.1 | 11.442 % |
c |    124484 |   14877    50289 |    5454    5316   265689    50.0 | 11.448 % |
c |    124635 |   14877    50289 |    6000    5467   270323    49.4 | 11.448 % |
c |    124860 |   14877    50289 |    6600    5692   292327    51.4 | 11.448 % |
c |    125197 |   14877    50289 |    7260    6029   329895    54.7 | 11.448 % |
c |    125703 |   14877    50289 |    7986    6535   361239    55.3 | 11.448 % |
c |    126462 |   14877    50289 |    8785    7294   391859    53.7 | 11.448 % |
c |    127603 |   14877    50289 |    9663    8435   478713    56.8 | 11.448 % |
c |    129311 |   14877    50289 |   10630   10143   570334    56.2 | 11.448 % |
c |    131874 |   14877    50289 |   11693    7035   309663    44.0 | 11.448 % |
c ==============================================================================
c Found solution: 1213440
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132830 |   14885    50302 |    4961    7990   344228    43.1 | 11.448 % |
c |    132930 |   14885    50302 |    5457    4095   130652    31.9 | 11.487 % |
c |    133082 |   14885    50302 |    6002    4247   140906    33.2 | 11.487 % |
c |    133308 |   14885    50302 |    6603    4473   145839    32.6 | 11.487 % |
c |    133645 |   14885    50302 |    7263    4810   163247    33.9 | 11.487 % |
c |    134152 |   14885    50302 |    7989    5317   180646    34.0 | 11.487 % |
c |    134911 |   14867    50262 |    8788    6074   210613    34.7 | 11.650 % |
c |    136050 |   14867    50262 |    9667    7213   249425    34.6 | 11.650 % |
c |    137760 |   14839    50199 |   10634    8921   304715    34.2 | 11.910 % |
c |    140322 |   14839    50199 |   11697   11483   433802    37.8 | 11.910 % |
c |    144166 |   14839    50199 |   12867    9063   353815    39.0 | 11.910 % |
c |    149933 |   14839    50199 |   14154    7885   325078    41.2 | 11.910 % |
c |    158582 |   14839    50199 |   15569    9129   370373    40.6 | 11.910 % |
c |    171556 |   14839    50199 |   17126   13879   596591    43.0 | 11.910 % |
c ==============================================================================
c Found solution: 1145856
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    183021 |   14849    50222 |    4949   16407   675729    41.2 | 11.910 % |
c |    183123 |   14849    50222 |    5443    4204   124504    29.6 | 11.927 % |
c |    183273 |   14849    50222 |    5988    4354   127342    29.2 | 11.927 % |
c |    183498 |   14849    50222 |    6587    4579   133579    29.2 | 11.927 % |
c |    183836 |   14849    50222 |    7245    4917   140722    28.6 | 11.927 % |
c |    184343 |   14849    50222 |    7970    5424   153528    28.3 | 11.927 % |
c |    185102 |   14849    50222 |    8767    6183   178163    28.8 | 11.927 % |
c |    186244 |   14849    50222 |    9644    7325   224903    30.7 | 11.927 % |
c |    187953 |   14849    50222 |   10608    9034   306970    34.0 | 11.927 % |
c |    190516 |   14849    50222 |   11669    5935   207351    34.9 | 11.927 % |
c |    194361 |   14849    50222 |   12836    9780   381421    39.0 | 11.927 % |
c |    200127 |   14849    50222 |   14120    8789   336369    38.3 | 11.927 % |
c |    208776 |   14849    50222 |   15532   10045   375187    37.4 | 11.927 % |
c |    221750 |   14849    50222 |   17085   14863   663052    44.6 | 11.927 % |
c ==============================================================================
c Found solution: 882688
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    226679 |   14815    50095 |    4938   10932   449646    41.1 | 11.927 % |
c |    226780 |   14815    50095 |    5431    2834    95029    33.5 | 12.131 % |
c |    226930 |   14815    50095 |    5974    2984   100132    33.6 | 12.131 % |
c |    227155 |   14815    50095 |    6572    3209   103870    32.4 | 12.131 % |
c |    227493 |   14815    50095 |    7229    3547   112944    31.8 | 12.131 % |
c |    228002 |   14815    50095 |    7952    4056   131115    32.3 | 12.131 % |
c |    228763 |   14815    50095 |    8747    4817   152790    31.7 | 12.131 % |
c |    229903 |   14815    50095 |    9622    5957   192874    32.4 | 12.131 % |
c |    231611 |   14815    50095 |   10585    7665   256994    33.5 | 12.131 % |
c |    234173 |   14815    50095 |   11643   10227   369004    36.1 | 12.131 % |
c |    238017 |   14815    50095 |   12807    7881   286356    36.3 | 12.131 % |
c |    243784 |   14815    50095 |   14088    6898   265127    38.4 | 12.131 % |
c |    252433 |   14725    49888 |   15497    8166   240170    29.4 | 13.104 % |
c |    265408 |   14698    49827 |   17047   12985   490542    37.8 | 13.428 % |
c ==============================================================================
c Found solution: 804864
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    267580 |   14710    49855 |    4903   15157   570717    37.7 | 13.428 % |
c |    267682 |   14710    49855 |    5393    3892   103008    26.5 | 13.430 % |
c |    267833 |   14710    49855 |    5932    4043   104747    25.9 | 13.430 % |
c |    268058 |   14710    49855 |    6525    4268   108961    25.5 | 13.430 % |
c |    268395 |   14710    49855 |    7178    4605   114605    24.9 | 13.430 % |
c |    268901 |   14710    49855 |    7896    5111   127137    24.9 | 13.430 % |
c |    269662 |   14710    49855 |    8685    5872   146984    25.0 | 13.430 % |
c |    270803 |   14710    49855 |    9554    7013   203504    29.0 | 13.430 % |
c |    272514 |   14710    49855 |   10510    8724   270568    31.0 | 13.430 % |
c |    275076 |   14710    49855 |   11561    5653   166684    29.5 | 13.430 % |
c |    278920 |   14710    49855 |   12717    9497   351916    37.1 | 13.430 % |
c |    284686 |   14697    49825 |   13988    8584   333786    38.9 | 13.592 % |
c |    293335 |   14697    49825 |   15387    9940   408374    41.1 | 13.592 % |
c |    306309 |   14697    49825 |   16926   14883   678759    45.6 | 13.592 % |
c |    325770 |   14697    49825 |   18619   16738   728728    43.5 | 13.592 % |
c |    354962 |   14697    49825 |   20481   16697   780600    46.8 | 13.592 % |
c |    398751 |   14673    49772 |   22529   18038   685094    38.0 | 13.819 % |
c |    464435 |   14665    49750 |   24782   13779   573078    41.6 | 13.884 % |
c |    562961 |   14665    49750 |   27260   22883  1101452    48.1 | 13.884 % |
c |    710752 |   14658    49735 |   29986   15376   652286    42.4 | 13.948 % |
c ==============================================================================
c Found solution: 623616
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    746664 |   14638    49690 |    4879   17992   706327    39.3 | 13.948 % |
c |    746764 |   14638    49690 |    5366    4598   126096    27.4 | 14.193 % |
c |    746914 |   14638    49690 |    5903    4748   127793    26.9 | 14.193 % |
c |    747139 |   14638    49690 |    6493    4973   134208    27.0 | 14.193 % |
c |    747476 |   14638    49690 |    7143    5310   144194    27.2 | 14.193 % |
c |    747983 |   14638    49690 |    7857    5817   154204    26.5 | 14.193 % |
c |    748742 |   14638    49690 |    8643    6576   178501    27.1 | 14.193 % |
c |    749883 |   14638    49690 |    9507    7717   235750    30.5 | 14.193 % |
c |    751592 |   14638    49690 |   10458    9426   293678    31.2 | 14.193 % |
c |    754155 |   14638    49690 |   11504    6266   192414    30.7 | 14.193 % |
c |    758000 |   14613    49633 |   12654   10109   337355    33.4 | 14.452 % |
c |    763767 |   14613    49633 |   13920    9088   320912    35.3 | 14.452 % |
c |    772417 |   14613    49633 |   15312   10244   395768    38.6 | 14.452 % |
c |    785392 |   14613    49633 |   16843   15023   729672    48.6 | 14.452 % |

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/20530/stat): 20530 (minisat+_script) R 20529 20530 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846732386 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/20530/statm): 174 3 169 147 0 27 0
[pid=20530] 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=20531
New process pid=20532
New process pid=20533
execve syscall for /bin/sed executable
One traced child (pid=20532) 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=20533) exited with status: 0
One traced child (pid=20531) exited with status: 0
New process pid=20534
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare1.opb

[startup+10.0038 s]
Raw data (loadavg): 1.06 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1005 0 0 0 983 4 0 0 25 0 1 0 1846732391 4399104 992 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20534/statm): 1074 992 145 145 0 929 0
[pid=20534] vsize: 4296
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 6420

[startup+20.0056 s]
Raw data (loadavg): 1.05 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1368 0 0 0 1976 7 0 0 25 0 1 0 1846732391 5906432 1355 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20534/statm): 1442 1355 145 145 0 1297 0
[pid=20534] vsize: 5768
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 7892

[startup+30.0073 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1555 0 0 0 2971 9 0 0 25 0 1 0 1846732391 6668288 1542 4294967295 134512640 135094434 3221224432 3221223104 134555763 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20534/statm): 1628 1542 145 145 0 1483 0
[pid=20534] vsize: 6512
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 8636

[startup+40.0081 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1555 0 0 0 3971 10 0 0 25 0 1 0 1846732391 6668288 1542 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20534/statm): 1628 1542 145 145 0 1483 0
[pid=20534] vsize: 6512
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 8636

[startup+50.0097 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1688 0 0 0 4968 12 0 0 25 0 1 0 1846732391 7213056 1675 4294967295 134512640 135094434 3221224432 3221223104 134556210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 1761 1675 145 145 0 1616 0
[pid=20534] vsize: 7044
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 9168

[startup+60.0105 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1688 0 0 0 5968 12 0 0 25 0 1 0 1846732391 7213056 1675 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 1761 1675 145 145 0 1616 0
[pid=20534] vsize: 7044
Current children cumulated CPU time (s) 59.81
Current children cumulated vsize (Kb) 9168

[startup+70.0122 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1846 0 0 0 6965 13 0 0 25 0 1 0 1846732391 7864320 1833 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 1920 1833 145 145 0 1775 0
[pid=20534] vsize: 7680
Current children cumulated CPU time (s) 69.79
Current children cumulated vsize (Kb) 9804

[startup+80.0129 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1897 0 0 0 7965 14 0 0 25 0 1 0 1846732391 8077312 1884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 1972 1884 145 145 0 1827 0
[pid=20534] vsize: 7888
Current children cumulated CPU time (s) 79.8
Current children cumulated vsize (Kb) 10012

[startup+90.0127 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 1905 0 0 0 8965 14 0 0 25 0 1 0 1846732391 8110080 1892 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 1980 1892 145 145 0 1835 0
[pid=20534] vsize: 7920
Current children cumulated CPU time (s) 89.8
Current children cumulated vsize (Kb) 10044

[startup+100.013 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2087 0 0 0 9962 15 0 0 25 0 1 0 1846732391 8921088 2074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2178 2074 145 145 0 2033 0
[pid=20534] vsize: 8712
Current children cumulated CPU time (s) 99.78
Current children cumulated vsize (Kb) 10836

[startup+110.014 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2098 0 0 0 10962 15 0 0 25 0 1 0 1846732391 8974336 2085 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2085 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 109.78
Current children cumulated vsize (Kb) 10888

[startup+120.015 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2100 0 0 0 11962 16 0 0 25 0 1 0 1846732391 8974336 2087 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2087 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 119.79
Current children cumulated vsize (Kb) 10888

[startup+130.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 12962 16 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 129.79
Current children cumulated vsize (Kb) 10888

[startup+140.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 13962 16 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 139.79
Current children cumulated vsize (Kb) 10888

[startup+150.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 14962 16 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 149.79
Current children cumulated vsize (Kb) 10888

[startup+160.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 15962 16 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223056 134562060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 159.79
Current children cumulated vsize (Kb) 10888

[startup+170.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 16962 16 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 169.79
Current children cumulated vsize (Kb) 10888

[startup+180.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 17963 16 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 179.8
Current children cumulated vsize (Kb) 10888

[startup+190.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 18963 16 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 189.8
Current children cumulated vsize (Kb) 10888

[startup+200.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 19963 16 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 199.8
Current children cumulated vsize (Kb) 10888

[startup+210.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 20963 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 209.81
Current children cumulated vsize (Kb) 10888

[startup+220.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 21963 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 219.81
Current children cumulated vsize (Kb) 10888

[startup+230.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 22964 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 229.82
Current children cumulated vsize (Kb) 10888

[startup+240.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 23964 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 239.82
Current children cumulated vsize (Kb) 10888

[startup+250.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 24964 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 249.82
Current children cumulated vsize (Kb) 10888

[startup+260.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 25964 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 259.82
Current children cumulated vsize (Kb) 10888

[startup+270.026 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 26964 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 269.82
Current children cumulated vsize (Kb) 10888

[startup+280.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 27965 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 279.83
Current children cumulated vsize (Kb) 10888

[startup+290.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 28965 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 289.83
Current children cumulated vsize (Kb) 10888

[startup+300.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 29965 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 299.83
Current children cumulated vsize (Kb) 10888

[startup+310.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 30965 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 309.83
Current children cumulated vsize (Kb) 10888

[startup+320.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 31965 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 319.83
Current children cumulated vsize (Kb) 10888

[startup+330.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 32965 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 329.83
Current children cumulated vsize (Kb) 10888

[startup+340.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 33965 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 339.83
Current children cumulated vsize (Kb) 10888

[startup+350.031 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 34966 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 349.84
Current children cumulated vsize (Kb) 10888

[startup+360.031 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2101 0 0 0 35966 17 0 0 25 0 1 0 1846732391 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2088 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 359.84
Current children cumulated vsize (Kb) 10888

[startup+370.032 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 36966 17 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223120 134554707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 369.84
Current children cumulated vsize (Kb) 10888

[startup+380.033 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 37966 17 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 379.84
Current children cumulated vsize (Kb) 10888

[startup+390.034 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 38966 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 389.85
Current children cumulated vsize (Kb) 10888

[startup+400.034 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 39966 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 399.85
Current children cumulated vsize (Kb) 10888

[startup+410.035 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 40966 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 409.85
Current children cumulated vsize (Kb) 10888

[startup+420.036 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 41967 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 419.86
Current children cumulated vsize (Kb) 10888

[startup+430.036 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 42967 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 429.86
Current children cumulated vsize (Kb) 10888

[startup+440.037 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 43967 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 439.86
Current children cumulated vsize (Kb) 10888

[startup+450.038 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 44967 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 449.86
Current children cumulated vsize (Kb) 10888

[startup+460.039 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 45967 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 459.86
Current children cumulated vsize (Kb) 10888

[startup+470.039 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 46967 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 469.86
Current children cumulated vsize (Kb) 10888

[startup+480.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 47968 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 479.87
Current children cumulated vsize (Kb) 10888

[startup+490.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2102 0 0 0 48968 18 0 0 25 0 1 0 1846732391 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2191 2089 145 145 0 2046 0
[pid=20534] vsize: 8764
Current children cumulated CPU time (s) 489.87
Current children cumulated vsize (Kb) 10888

[startup+500.042 s]
Raw data (loadavg): 1.07 1.01 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2136 0 0 0 49968 18 0 0 25 0 1 0 1846732391 9113600 2123 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2225 2123 145 145 0 2080 0
[pid=20534] vsize: 8900
Current children cumulated CPU time (s) 499.87
Current children cumulated vsize (Kb) 11024

[startup+510.042 s]
Raw data (loadavg): 1.06 1.01 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2144 0 0 0 50968 18 0 0 25 0 1 0 1846732391 9146368 2131 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2233 2131 145 145 0 2088 0
[pid=20534] vsize: 8932
Current children cumulated CPU time (s) 509.87
Current children cumulated vsize (Kb) 11056

[startup+520.043 s]
Raw data (loadavg): 1.05 1.01 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2202 0 0 0 51967 19 0 0 25 0 1 0 1846732391 9375744 2189 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2289 2189 145 145 0 2144 0
[pid=20534] vsize: 9156
Current children cumulated CPU time (s) 519.87
Current children cumulated vsize (Kb) 11280

[startup+530.044 s]
Raw data (loadavg): 1.04 1.01 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2279 0 0 0 52966 19 0 0 25 0 1 0 1846732391 9691136 2266 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2366 2266 145 145 0 2221 0
[pid=20534] vsize: 9464
Current children cumulated CPU time (s) 529.86
Current children cumulated vsize (Kb) 11588

[startup+540.044 s]
Raw data (loadavg): 1.04 1.01 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2422 0 0 0 53965 20 0 0 25 0 1 0 1846732391 10289152 2409 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2512 2409 145 145 0 2367 0
[pid=20534] vsize: 10048
Current children cumulated CPU time (s) 539.86
Current children cumulated vsize (Kb) 12172

[startup+550.044 s]
Raw data (loadavg): 1.03 1.01 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2429 0 0 0 54964 21 0 0 25 0 1 0 1846732391 10321920 2416 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2520 2416 145 145 0 2375 0
[pid=20534] vsize: 10080
Current children cumulated CPU time (s) 549.86
Current children cumulated vsize (Kb) 12204

[startup+560.045 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2439 0 0 0 55965 21 0 0 25 0 1 0 1846732391 10371072 2426 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2532 2426 145 145 0 2387 0
[pid=20534] vsize: 10128
Current children cumulated CPU time (s) 559.87
Current children cumulated vsize (Kb) 12252

[startup+570.046 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2441 0 0 0 56965 21 0 0 25 0 1 0 1846732391 10379264 2428 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2534 2428 145 145 0 2389 0
[pid=20534] vsize: 10136
Current children cumulated CPU time (s) 569.87
Current children cumulated vsize (Kb) 12260

[startup+580.046 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2451 0 0 0 57963 22 0 0 25 0 1 0 1846732391 10428416 2438 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2546 2438 145 145 0 2401 0
[pid=20534] vsize: 10184
Current children cumulated CPU time (s) 579.86
Current children cumulated vsize (Kb) 12308

[startup+590.047 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2459 0 0 0 58963 22 0 0 25 0 1 0 1846732391 10477568 2446 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2558 2446 145 145 0 2413 0
[pid=20534] vsize: 10232
Current children cumulated CPU time (s) 589.86
Current children cumulated vsize (Kb) 12356

[startup+600.048 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2467 0 0 0 59963 23 0 0 25 0 1 0 1846732391 10510336 2454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2566 2454 145 145 0 2421 0
[pid=20534] vsize: 10264
Current children cumulated CPU time (s) 599.87
Current children cumulated vsize (Kb) 12388

[startup+610.049 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2510 0 0 0 60962 23 0 0 25 0 1 0 1846732391 10702848 2497 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2613 2497 145 145 0 2468 0
[pid=20534] vsize: 10452
Current children cumulated CPU time (s) 609.86
Current children cumulated vsize (Kb) 12576

[startup+620.049 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2516 0 0 0 61962 24 0 0 25 0 1 0 1846732391 10727424 2503 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2619 2503 145 145 0 2474 0
[pid=20534] vsize: 10476
Current children cumulated CPU time (s) 619.87
Current children cumulated vsize (Kb) 12600

[startup+630.05 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2567 0 0 0 62961 24 0 0 25 0 1 0 1846732391 10936320 2554 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2670 2554 145 145 0 2525 0
[pid=20534] vsize: 10680
Current children cumulated CPU time (s) 629.86
Current children cumulated vsize (Kb) 12804

[startup+640.051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2575 0 0 0 63961 25 0 0 25 0 1 0 1846732391 10969088 2562 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2678 2562 145 145 0 2533 0
[pid=20534] vsize: 10712
Current children cumulated CPU time (s) 639.87
Current children cumulated vsize (Kb) 12836

[startup+650.052 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2577 0 0 0 64961 25 0 0 25 0 1 0 1846732391 10977280 2564 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2680 2564 145 145 0 2535 0
[pid=20534] vsize: 10720
Current children cumulated CPU time (s) 649.87
Current children cumulated vsize (Kb) 12844

[startup+660.051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2590 0 0 0 65961 25 0 0 25 0 1 0 1846732391 11030528 2577 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2693 2577 145 145 0 2548 0
[pid=20534] vsize: 10772
Current children cumulated CPU time (s) 659.87
Current children cumulated vsize (Kb) 12896

[startup+670.053 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2611 0 0 0 66961 25 0 0 25 0 1 0 1846732391 11145216 2598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2721 2598 145 145 0 2576 0
[pid=20534] vsize: 10884
Current children cumulated CPU time (s) 669.87
Current children cumulated vsize (Kb) 13008

[startup+680.054 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2628 0 0 0 67962 25 0 0 25 0 1 0 1846732391 11218944 2615 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2739 2615 145 145 0 2594 0
[pid=20534] vsize: 10956
Current children cumulated CPU time (s) 679.88
Current children cumulated vsize (Kb) 13080

[startup+690.054 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2639 0 0 0 68961 25 0 0 25 0 1 0 1846732391 11268096 2626 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2751 2626 145 145 0 2606 0
[pid=20534] vsize: 11004
Current children cumulated CPU time (s) 689.87
Current children cumulated vsize (Kb) 13128

[startup+700.056 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2639 0 0 0 69962 25 0 0 25 0 1 0 1846732391 11268096 2626 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2751 2626 145 145 0 2606 0
[pid=20534] vsize: 11004
Current children cumulated CPU time (s) 699.88
Current children cumulated vsize (Kb) 13128

[startup+710.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2756 0 0 0 70960 26 0 0 25 0 1 0 1846732391 11735040 2743 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2865 2743 145 145 0 2720 0
[pid=20534] vsize: 11460
Current children cumulated CPU time (s) 709.87
Current children cumulated vsize (Kb) 13584

[startup+720.058 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2766 0 0 0 71959 27 0 0 25 0 1 0 1846732391 11784192 2753 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2877 2753 145 145 0 2732 0
[pid=20534] vsize: 11508
Current children cumulated CPU time (s) 719.87
Current children cumulated vsize (Kb) 13632

[startup+730.058 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2815 0 0 0 72959 27 0 0 25 0 1 0 1846732391 11988992 2802 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2927 2802 145 145 0 2782 0
[pid=20534] vsize: 11708
Current children cumulated CPU time (s) 729.87
Current children cumulated vsize (Kb) 13832

[startup+740.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2816 0 0 0 73959 27 0 0 25 0 1 0 1846732391 11988992 2803 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2927 2803 145 145 0 2782 0
[pid=20534] vsize: 11708
Current children cumulated CPU time (s) 739.87
Current children cumulated vsize (Kb) 13832

[startup+750.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2816 0 0 0 74959 27 0 0 25 0 1 0 1846732391 11988992 2803 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2927 2803 145 145 0 2782 0
[pid=20534] vsize: 11708
Current children cumulated CPU time (s) 749.87
Current children cumulated vsize (Kb) 13832

[startup+760.061 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2825 0 0 0 75959 27 0 0 25 0 1 0 1846732391 12034048 2812 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2938 2812 145 145 0 2793 0
[pid=20534] vsize: 11752
Current children cumulated CPU time (s) 759.87
Current children cumulated vsize (Kb) 13876

[startup+770.062 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2875 0 0 0 76959 28 0 0 25 0 1 0 1846732391 12234752 2862 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2987 2862 145 145 0 2842 0
[pid=20534] vsize: 11948
Current children cumulated CPU time (s) 769.88
Current children cumulated vsize (Kb) 14072

[startup+780.063 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2875 0 0 0 77959 28 0 0 25 0 1 0 1846732391 12234752 2862 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 2987 2862 145 145 0 2842 0
[pid=20534] vsize: 11948
Current children cumulated CPU time (s) 779.88
Current children cumulated vsize (Kb) 14072

[startup+790.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2937 0 0 0 78958 28 0 0 25 0 1 0 1846732391 12500992 2924 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3052 2924 145 145 0 2907 0
[pid=20534] vsize: 12208
Current children cumulated CPU time (s) 789.87
Current children cumulated vsize (Kb) 14332

[startup+800.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2947 0 0 0 79959 28 0 0 25 0 1 0 1846732391 12550144 2934 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3064 2934 145 145 0 2919 0
[pid=20534] vsize: 12256
Current children cumulated CPU time (s) 799.88
Current children cumulated vsize (Kb) 14380

[startup+810.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2979 0 0 0 80959 28 0 0 25 0 1 0 1846732391 12693504 2966 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3099 2966 145 145 0 2954 0
[pid=20534] vsize: 12396
Current children cumulated CPU time (s) 809.88
Current children cumulated vsize (Kb) 14520

[startup+820.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2979 0 0 0 81959 28 0 0 25 0 1 0 1846732391 12693504 2966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3099 2966 145 145 0 2954 0
[pid=20534] vsize: 12396
Current children cumulated CPU time (s) 819.88
Current children cumulated vsize (Kb) 14520

[startup+830.067 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2983 0 0 0 82959 28 0 0 25 0 1 0 1846732391 12709888 2970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3103 2970 145 145 0 2958 0
[pid=20534] vsize: 12412
Current children cumulated CPU time (s) 829.88
Current children cumulated vsize (Kb) 14536

[startup+840.067 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 2994 0 0 0 83959 28 0 0 25 0 1 0 1846732391 12754944 2981 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3114 2981 145 145 0 2969 0
[pid=20534] vsize: 12456
Current children cumulated CPU time (s) 839.88
Current children cumulated vsize (Kb) 14580

[startup+850.068 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3012 0 0 0 84959 28 0 0 25 0 1 0 1846732391 12836864 2999 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20534/statm): 3134 2999 145 145 0 2989 0
[pid=20534] vsize: 12536
Current children cumulated CPU time (s) 849.88
Current children cumulated vsize (Kb) 14660

[startup+860.069 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3102 0 0 0 85957 29 0 0 25 0 1 0 1846732391 13201408 3089 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3223 3089 145 145 0 3078 0
[pid=20534] vsize: 12892
Current children cumulated CPU time (s) 859.87
Current children cumulated vsize (Kb) 15016

[startup+870.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3105 0 0 0 86957 29 0 0 25 0 1 0 1846732391 13217792 3092 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3227 3092 145 145 0 3082 0
[pid=20534] vsize: 12908
Current children cumulated CPU time (s) 869.87
Current children cumulated vsize (Kb) 15032

[startup+880.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3110 0 0 0 87958 29 0 0 25 0 1 0 1846732391 13250560 3097 4294967295 134512640 135094434 3221224432 3221223104 134556515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3235 3097 145 145 0 3090 0
[pid=20534] vsize: 12940
Current children cumulated CPU time (s) 879.88
Current children cumulated vsize (Kb) 15064

[startup+890.072 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3110 0 0 0 88958 29 0 0 25 0 1 0 1846732391 13250560 3097 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3235 3097 145 145 0 3090 0
[pid=20534] vsize: 12940
Current children cumulated CPU time (s) 889.88
Current children cumulated vsize (Kb) 15064

[startup+900.073 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3115 0 0 0 89958 29 0 0 25 0 1 0 1846732391 13275136 3102 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3241 3102 145 145 0 3096 0
[pid=20534] vsize: 12964
Current children cumulated CPU time (s) 899.88
Current children cumulated vsize (Kb) 15088

[startup+910.074 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3115 0 0 0 90958 29 0 0 25 0 1 0 1846732391 13275136 3102 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3241 3102 145 145 0 3096 0
[pid=20534] vsize: 12964
Current children cumulated CPU time (s) 909.88
Current children cumulated vsize (Kb) 15088

[startup+920.074 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3115 0 0 0 91958 30 0 0 25 0 1 0 1846732391 13275136 3102 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20534/statm): 3241 3102 145 145 0 3096 0
[pid=20534] vsize: 12964
Current children cumulated CPU time (s) 919.89
Current children cumulated vsize (Kb) 15088

[startup+930.075 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3115 0 0 0 92958 30 0 0 25 0 1 0 1846732391 13275136 3102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20534/statm): 3241 3102 145 145 0 3096 0
[pid=20534] vsize: 12964
Current children cumulated CPU time (s) 929.89
Current children cumulated vsize (Kb) 15088

[startup+940.076 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3115 0 0 0 93958 30 0 0 25 0 1 0 1846732391 13275136 3102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3241 3102 145 145 0 3096 0
[pid=20534] vsize: 12964
Current children cumulated CPU time (s) 939.89
Current children cumulated vsize (Kb) 15088

[startup+950.077 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3183 0 0 0 94956 30 0 0 25 0 1 0 1846732391 13565952 3170 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3312 3170 145 145 0 3167 0
[pid=20534] vsize: 13248
Current children cumulated CPU time (s) 949.87
Current children cumulated vsize (Kb) 15372

[startup+960.078 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3190 0 0 0 95957 30 0 0 25 0 1 0 1846732391 13598720 3177 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3320 3177 145 145 0 3175 0
[pid=20534] vsize: 13280
Current children cumulated CPU time (s) 959.88
Current children cumulated vsize (Kb) 15404

[startup+970.079 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3194 0 0 0 96957 31 0 0 25 0 1 0 1846732391 13615104 3181 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3324 3181 145 145 0 3179 0
[pid=20534] vsize: 13296
Current children cumulated CPU time (s) 969.89
Current children cumulated vsize (Kb) 15420

[startup+980.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3277 0 0 0 97956 31 0 0 25 0 1 0 1846732391 13967360 3264 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3410 3264 145 145 0 3265 0
[pid=20534] vsize: 13640
Current children cumulated CPU time (s) 979.88
Current children cumulated vsize (Kb) 15764

[startup+990.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3279 0 0 0 98956 32 0 0 25 0 1 0 1846732391 14000128 3266 4294967295 134512640 135094434 3221224432 3221223024 134557253 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3418 3266 145 145 0 3273 0
[pid=20534] vsize: 13672
Current children cumulated CPU time (s) 989.89
Current children cumulated vsize (Kb) 15796

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.97 1/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) T 20530 20530 2660 0 -1 0 3283 0 0 0 99956 32 0 0 25 0 1 0 1846732391 14000128 3270 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3418 3270 145 145 0 3273 0
[pid=20534] vsize: 13672
Current children cumulated CPU time (s) 999.89
Current children cumulated vsize (Kb) 15796

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3312 0 0 0 100955 32 0 0 25 0 1 0 1846732391 14118912 3299 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3447 3299 145 145 0 3302 0
[pid=20534] vsize: 13788
Current children cumulated CPU time (s) 1009.88
Current children cumulated vsize (Kb) 15912

[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3326 0 0 0 101955 32 0 0 25 0 1 0 1846732391 14184448 3313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3463 3313 145 145 0 3318 0
[pid=20534] vsize: 13852
Current children cumulated CPU time (s) 1019.88
Current children cumulated vsize (Kb) 15976

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3343 0 0 0 102955 32 0 0 25 0 1 0 1846732391 14254080 3330 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3480 3330 145 145 0 3335 0
[pid=20534] vsize: 13920
Current children cumulated CPU time (s) 1029.88
Current children cumulated vsize (Kb) 16044

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3343 0 0 0 103955 32 0 0 25 0 1 0 1846732391 14254080 3330 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3480 3330 145 145 0 3335 0
[pid=20534] vsize: 13920
Current children cumulated CPU time (s) 1039.88
Current children cumulated vsize (Kb) 16044

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3343 0 0 0 104955 32 0 0 25 0 1 0 1846732391 14254080 3330 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3480 3330 145 145 0 3335 0
[pid=20534] vsize: 13920
Current children cumulated CPU time (s) 1049.88
Current children cumulated vsize (Kb) 16044

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3343 0 0 0 105955 33 0 0 25 0 1 0 1846732391 14254080 3330 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3480 3330 145 145 0 3335 0
[pid=20534] vsize: 13920
Current children cumulated CPU time (s) 1059.89
Current children cumulated vsize (Kb) 16044

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3348 0 0 0 106956 33 0 0 25 0 1 0 1846732391 14286848 3335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3488 3335 145 145 0 3343 0
[pid=20534] vsize: 13952
Current children cumulated CPU time (s) 1069.9
Current children cumulated vsize (Kb) 16076

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3360 0 0 0 107956 33 0 0 25 0 1 0 1846732391 14352384 3347 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3347 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1079.9
Current children cumulated vsize (Kb) 16140

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3360 0 0 0 108956 33 0 0 25 0 1 0 1846732391 14352384 3347 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3347 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1089.9
Current children cumulated vsize (Kb) 16140

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3360 0 0 0 109956 33 0 0 25 0 1 0 1846732391 14352384 3347 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3347 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1099.9
Current children cumulated vsize (Kb) 16140

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3361 0 0 0 110956 33 0 0 25 0 1 0 1846732391 14352384 3348 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20534/statm): 3504 3348 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1109.9
Current children cumulated vsize (Kb) 16140

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3361 0 0 0 111956 33 0 0 25 0 1 0 1846732391 14352384 3348 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3348 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1119.9
Current children cumulated vsize (Kb) 16140

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 112956 33 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1129.9
Current children cumulated vsize (Kb) 16140

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 113956 33 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1139.9
Current children cumulated vsize (Kb) 16140

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 114956 33 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1149.9
Current children cumulated vsize (Kb) 16140

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 115956 33 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1159.9
Current children cumulated vsize (Kb) 16140

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 116956 33 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1169.9
Current children cumulated vsize (Kb) 16140

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 117955 35 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1179.91
Current children cumulated vsize (Kb) 16140

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 118955 35 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1189.91
Current children cumulated vsize (Kb) 16140

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 119955 35 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1199.91
Current children cumulated vsize (Kb) 16140

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 120955 36 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1209.92
Current children cumulated vsize (Kb) 16140



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 20534
Raw data (/proc/20530/stat): 20530 (minisat+_script) S 20529 20530 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1846732386 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20530/statm): 531 226 485 147 0 384 0
[pid=20530] vsize: 2124
Raw data (/proc/20534/stat): 20534 (minisat+_64-bit) R 20530 20530 2660 0 -1 0 3363 0 0 0 120955 36 0 0 25 0 1 0 1846732391 14352384 3350 4294967295 134512640 135094434 3221224432 3221223104 134556499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20534/statm): 3504 3350 145 145 0 3359 0
[pid=20534] vsize: 14016
Current children cumulated CPU time (s) 1209.92
Current children cumulated vsize (Kb) 16140

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.92
CPU user time (s): 1209.56
CPU system time (s): 0.366944
CPU usage (%): 99.9848
Max. virtual memory (cumulated for all children) (Kb): 16140

Verifier Data

ERROR: no interpretation found !