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/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare2_1.opb
MD5SUMa84a96a9314212f3d8ecd5227c500cef
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 63179
Optimality of the best value was proved NO
Number of terms in the objective function 210
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 7516192761
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 7516192761
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.03
Number of variables330
Total number of constraints67
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)54
Number of constraints which are nor clauses,nor cardinality constraints13
Minimum length of a constraint1
Maximum length of a constraint150

Trace number 5887

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        903096 kB
Buffers:         20376 kB
Cached:          86596 kB
SwapCached:        740 kB
Active:          30320 kB
Inactive:        79364 kB
HighTotal:      131008 kB
HighFree:        42644 kB
LowTotal:       903652 kB
LowFree:        860452 kB
SwapTotal:     2097136 kB
SwapFree:      2095892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            16112 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 01:48:19 (client local time) WITH STATUS 10 IN 1209.27 SECONDS
stats: 3059 7 1209.27 10

Solver Data

c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  12]---> Adder-cost: 708   maxlim: 3756758   bits: 23/22
c ---[  10]---> Adder-cost: 758   maxlim: 4064912   bits: 23/22
c ---[   8]---> Adder-cost: 714   maxlim: 3859164   bits: 23/22
c ---[   6]---> Adder-cost: 676   maxlim: 4153021   bits: 23/22
c ---[   4]---> Adder-cost: 812   maxlim: 3812158   bits: 23/22
c ---[   2]---> Adder-cost: 766   maxlim: 4131466   bits: 23/22
c ---[   0]---> Adder-cost: 692   maxlim: 3780388   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   34933   124179 |   11644       0        0     nan |  0.000 % |
c |       100 |   34933   124179 |   12808     100      416     4.2 |  6.830 % |
c |       250 |   34933   124179 |   14089     250     1526     6.1 |  6.830 % |
c |       475 |   34933   124179 |   15498     475     3526     7.4 |  6.830 % |
c ==============================================================================
c Found solution: 8658716
c ---[   0]---> Sorter-cost: 2158     Base: 2 2 2 2 2 2 2 2 2 2 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 |       805 |   40455   137066 |   13485     804     7989     9.9 |  6.830 % |
c ==============================================================================
c Found solution: 5260062
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 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 |       835 |   40500   137210 |   13500     834     8278     9.9 |  6.830 % |
c |       935 |   40492   137184 |   14850     933     9140     9.8 |  5.136 % |
c |      1085 |   40460   137080 |   16335    1079    10291     9.5 |  5.189 % |
c |      1310 |   40460   137080 |   17968    1304    11927     9.1 |  5.189 % |
c |      1647 |   40460   137080 |   19765    1641    13700     8.3 |  5.189 % |
c |      2154 |   40436   137002 |   21741    2145    20816     9.7 |  5.228 % |
c |      2914 |   40428   136976 |   23916    2904    37504    12.9 |  5.242 % |
c |      4054 |   40428   136976 |   26307    4044    60613    15.0 |  5.242 % |
c ==============================================================================
c Found solution: 4950048
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 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 |      4373 |   40449   137020 |   13483    4356    90869    20.9 |  5.242 % |
c |      4473 |   40449   137020 |   14831    4456    93625    21.0 |  5.271 % |
c |      4623 |   40449   137020 |   16314    4606    94532    20.5 |  5.271 % |
c |      4848 |   40449   137020 |   17945    4831    97424    20.2 |  5.271 % |
c |      5186 |   40449   137020 |   19740    5169   101715    19.7 |  5.271 % |
c |      5693 |   40449   137020 |   21714    5676   114014    20.1 |  5.271 % |
c |      6452 |   40449   137020 |   23885    6435   142255    22.1 |  5.271 % |
c ==============================================================================
c Found solution: 4620607
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 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 |      6683 |   40491   137120 |   13497    6666   159247    23.9 |  5.271 % |
c |      6783 |   40483   137094 |   14846    6765   160692    23.8 |  5.282 % |
c |      6933 |   40483   137094 |   16331    6915   164982    23.9 |  5.282 % |
c |      7158 |   40483   137094 |   17964    7140   169116    23.7 |  5.282 % |
c |      7495 |   40483   137094 |   19760    7477   174450    23.3 |  5.282 % |
c |      8004 |   40467   137042 |   21737    7984   180282    22.6 |  5.308 % |
c |      8763 |   40461   137024 |   23910    8742   191914    22.0 |  5.321 % |
c |      9902 |   40453   136998 |   26301    9880   257083    26.0 |  5.335 % |
c |     11611 |   40453   136998 |   28932   11589   499552    43.1 |  5.335 % |
c ==============================================================================
c Found solution: 4249759
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 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 |     11737 |   40475   137049 |   13491   11715   502214    42.9 |  5.335 % |
c |     11837 |   40475   137049 |   14840   11815   507717    43.0 |  5.341 % |
c |     11987 |   40475   137049 |   16324   11965   515534    43.1 |  5.341 % |
c |     12212 |   40475   137049 |   17956   12190   524302    43.0 |  5.341 % |
c |     12550 |   40475   137049 |   19752   12528   540452    43.1 |  5.341 % |
c |     13056 |   40467   137023 |   21727   13033   550988    42.3 |  5.354 % |
c |     13815 |   40467   137023 |   23900   13792   578807    42.0 |  5.354 % |
c |     14955 |   40467   137023 |   26290   14932   644252    43.1 |  5.354 % |
c ==============================================================================
c Found solution: 3339853
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 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 |     15826 |   40493   137087 |   13497   15803   672645    42.6 |  5.354 % |
c |     15926 |   40493   137087 |   14846    8002   416550    52.1 |  5.356 % |
c |     16076 |   40493   137087 |   16331    8152   422105    51.8 |  5.356 % |
c |     16301 |   40493   137087 |   17964    8377   437923    52.3 |  5.356 % |
c |     16638 |   40493   137087 |   19760    8714   445487    51.1 |  5.356 % |
c |     17144 |   40493   137087 |   21737    9220   455219    49.4 |  5.356 % |
c ==============================================================================
c Found solution: 3334229
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 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 |     17762 |   40515   137139 |   13505    9838   522989    53.2 |  5.356 % |
c |     17863 |   40515   137139 |   14855    9939   525768    52.9 |  5.363 % |
c |     18013 |   40515   137139 |   16341   10089   527063    52.2 |  5.363 % |
c |     18241 |   40515   137139 |   17975   10317   529533    51.3 |  5.363 % |
c |     18578 |   40515   137139 |   19772   10654   536878    50.4 |  5.363 % |
c ==============================================================================
c Found solution: 3287413
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 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 |     19079 |   40536   137188 |   13512   11155   547166    49.1 |  5.363 % |
c |     19180 |   40536   137188 |   14863   11256   550369    48.9 |  5.368 % |
c |     19330 |   40536   137188 |   16349   11406   553026    48.5 |  5.368 % |
c |     19555 |   40536   137188 |   17984   11631   558823    48.0 |  5.368 % |
c |     19893 |   40536   137188 |   19782   11969   572765    47.9 |  5.368 % |
c |     20399 |   40528   137162 |   21761   12474   580989    46.6 |  5.381 % |
c |     21158 |   40522   137149 |   23937   13228   596004    45.1 |  5.407 % |
c ==============================================================================
c Found solution: 2290547
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 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 |     21322 |   40544   137206 |   13514   13392   600636    44.9 |  5.407 % |
c |     21422 |   40544   137206 |   14865   13492   604346    44.8 |  5.412 % |
c |     21573 |   40544   137206 |   16351   13643   607938    44.6 |  5.412 % |
c |     21798 |   40544   137206 |   17987   13868   614171    44.3 |  5.412 % |
c |     22135 |   40544   137206 |   19785   14205   624729    44.0 |  5.412 % |
c |     22644 |   40544   137206 |   21764   14714   638820    43.4 |  5.412 % |
c |     23404 |   40544   137206 |   23940   15474   661163    42.7 |  5.412 % |
c |     24543 |   40544   137206 |   26334   16613   721090    43.4 |  5.412 % |
c |     26252 |   40544   137206 |   28968   18322   789853    43.1 |  5.412 % |
c |     28815 |   40544   137206 |   31865   20885   905885    43.4 |  5.412 % |
c |     32661 |   40535   137179 |   35051   24730  1011947    40.9 |  5.438 % |
c |     38427 |   40535   137179 |   38557   30496  1345865    44.1 |  5.438 % |
c ==============================================================================
c Found solution: 1436307
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 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 |     45811 |   40559   137239 |   13519   37880  1653565    43.7 |  5.438 % |
c |     45912 |   40559   137239 |   14870    7144   239022    33.5 |  5.440 % |
c |     46063 |   40559   137239 |   16357    7295   247734    34.0 |  5.440 % |
c |     46288 |   40559   137239 |   17993    7520   249720    33.2 |  5.440 % |
c |     46627 |   40559   137239 |   19793    7859   253146    32.2 |  5.440 % |
c |     47134 |   40559   137239 |   21772    8366   269347    32.2 |  5.440 % |
c |     47893 |   40559   137239 |   23949    9125   361442    39.6 |  5.440 % |
c |     49032 |   40559   137239 |   26344   10264   396132    38.6 |  5.440 % |
c |     50741 |   40559   137239 |   28979   11973   437100    36.5 |  5.440 % |
c |     53303 |   40559   137239 |   31877   14535   538464    37.0 |  5.440 % |
c ==============================================================================
c Found solution: 1226125
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 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 |     53727 |   40579   137287 |   13526   14959   548574    36.7 |  5.440 % |
c |     53828 |   40579   137287 |   14878    7581   202510    26.7 |  5.445 % |
c |     53978 |   40579   137287 |   16366    7731   204888    26.5 |  5.445 % |
c |     54204 |   40579   137287 |   18003    7957   208315    26.2 |  5.445 % |
c |     54542 |   40579   137287 |   19803    8295   216444    26.1 |  5.445 % |
c |     55048 |   40579   137287 |   21783    8801   224770    25.5 |  5.445 % |
c |     55809 |   40579   137287 |   23962    9562   252224    26.4 |  5.445 % |
c |     56950 |   40579   137287 |   26358   10703   296178    27.7 |  5.445 % |
c |     58660 |   40573   137269 |   28994   12412   374420    30.2 |  5.458 % |
c |     61223 |   40573   137269 |   31893   14975   496937    33.2 |  5.458 % |
c |     65067 |   40573   137269 |   35082   18819   695359    36.9 |  5.458 % |
c |     70834 |   40573   137269 |   38591   24586   924178    37.6 |  5.458 % |
c |     79483 |   40547   137211 |   42450   33229  1386072    41.7 |  5.549 % |
c |     92457 |   40547   137211 |   46695   16206   718044    44.3 |  5.549 % |
c |    111919 |   40547   137211 |   51364   35668  1877866    52.6 |  5.549 % |
c |    141112 |   40547   137211 |   56501   26554  1476960    55.6 |  5.549 % |
c |    184902 |   40547   137211 |   62151   25536  2450937    96.0 |  5.549 % |
c |    250586 |   40535   137180 |   68366   43565  2228582    51.2 |  5.588 % |
c |    349114 |   40535   137180 |   75203   35537  2570698    72.3 |  5.588 % |
c |    496904 |   40535   137180 |   82723   63098  3631157    57.5 |  5.588 % |
c ==============================================================================
c Found solution: 937675
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 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 |    611637 |   40477   136981 |   13492   41360  3147226    76.1 |  5.588 % |
c |    611737 |   40477   136981 |   14841    7432   636521    85.6 |  5.761 % |
c |    611887 |   40477   136981 |   16325    7582   639768    84.4 |  5.761 % |
c |    612112 |   40477   136981 |   17957    7807   641772    82.2 |  5.761 % |
c |    612449 |   40477   136981 |   19753    8144   651973    80.1 |  5.761 % |
c |    612956 |   40477   136981 |   21729    8651   667626    77.2 |  5.761 % |
c |    613717 |   40477   136981 |   23901    9412   691168    73.4 |  5.761 % |
c |    614857 |   40477   136981 |   26292   10552   723865    68.6 |  5.761 % |
c |    616566 |   40477   136981 |   28921   12261   788603    64.3 |  5.761 % |
c |    619128 |   40472   136970 |   31813   14822   938756    63.3 |  5.787 % |
c |    622973 |   40472   136970 |   34994   18667  1092890    58.5 |  5.787 % |
c |    628739 |   40472   136970 |   38494   24433  1322315    54.1 |  5.787 % |
c |    637388 |   40448   136917 |   42343   33079  1753094    53.0 |  5.892 % |
c |    650363 |   40404   136818 |   46578   17084   937926    54.9 |  6.061 % |
c |    669828 |   40396   136796 |   51235   36548  1867018    51.1 |  6.087 % |
c |    699020 |   40396   136796 |   56359   27623  1424195    51.6 |  6.087 % |
c |    742811 |   40396   136796 |   61995   27073  1822699    67.3 |  6.087 % |
c ==============================================================================
c Found solution: 681120
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 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 |    749104 |   40314   136607 |   13438   33351  2060389    61.8 |  6.087 % |
c |    749204 |   40314   136607 |   14781    7777   221057    28.4 |  6.533 % |
c |    749355 |   40314   136607 |   16259    7928   223104    28.1 |  6.533 % |
c |    749580 |   40314   136607 |   17885    8153   227139    27.9 |  6.533 % |
c |    749918 |   40314   136607 |   19674    8491   236519    27.9 |  6.533 % |
c |    750424 |   40314   136607 |   21642    8997   248399    27.6 |  6.533 % |
c |    751183 |   40314   136607 |   23806    9756   265928    27.3 |  6.533 % |
c |    752322 |   40314   136607 |   26186   10895   306954    28.2 |  6.533 % |
c |    754030 |   40314   136607 |   28805   12603   375521    29.8 |  6.533 % |
c |    756592 |   40314   136607 |   31686   15165   477461    31.5 |  6.533 % |
c |    760437 |   40314   136607 |   34854   19010   626240    32.9 |  6.533 % |
c |    766203 |   40314   136607 |   38340   24776   878769    35.5 |  6.533 % |
c |    774852 |   40314   136607 |   42174   33425  1385351    41.4 |  6.533 % |

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/24008/stat): 24008 (minisat+_script) R 24007 24008 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796353810 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24008/statm): 174 3 169 147 0 27 0
[pid=24008] 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=24009
New process pid=24010
New process pid=24011
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
One traced child (pid=24010) exited with status: 0
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=24011) exited with status: 0
One traced child (pid=24009) exited with status: 0
New process pid=24012
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare2_1.opb

[startup+10.005 s]
Raw data (loadavg): 0.93 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 1576 0 0 0 981 5 0 0 25 0 1 0 1796353815 6766592 1529 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 1652 1529 145 145 0 1507 0
[pid=24012] vsize: 6608
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 8732

[startup+20.0058 s]
Raw data (loadavg): 0.94 0.98 0.98 1/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) T 24008 24008 824 0 -1 0 1925 0 0 0 1976 7 0 0 25 0 1 0 1796353815 8179712 1878 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24012/statm): 1997 1878 145 145 0 1852 0
[pid=24012] vsize: 7988
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 10112

[startup+30.0065 s]
Raw data (loadavg): 0.95 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 2722 0 0 0 2961 13 0 0 25 0 1 0 1796353815 11448320 2675 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24012/statm): 2795 2675 145 145 0 2650 0
[pid=24012] vsize: 11180
Current children cumulated CPU time (s) 29.76
Current children cumulated vsize (Kb) 13304

[startup+40.0072 s]
Raw data (loadavg): 0.96 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3098 0 0 0 3954 15 0 0 25 0 1 0 1796353815 13094912 3051 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 3197 3051 145 145 0 3052 0
[pid=24012] vsize: 12788
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 14912

[startup+50.008 s]
Raw data (loadavg): 0.96 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3098 0 0 0 4954 15 0 0 25 0 1 0 1796353815 13094912 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 3197 3051 145 145 0 3052 0
[pid=24012] vsize: 12788
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 14912

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3098 0 0 0 5955 15 0 0 25 0 1 0 1796353815 13094912 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24012/statm): 3197 3051 145 145 0 3052 0
[pid=24012] vsize: 12788
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 14912

[startup+70.0095 s]
Raw data (loadavg): 0.97 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3514 0 0 0 6945 18 0 0 25 0 1 0 1796353815 14774272 3467 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 3607 3467 145 145 0 3462 0
[pid=24012] vsize: 14428
Current children cumulated CPU time (s) 69.65
Current children cumulated vsize (Kb) 16552

[startup+80.0102 s]
Raw data (loadavg): 0.98 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3566 0 0 0 7944 19 0 0 25 0 1 0 1796353815 14987264 3519 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 3659 3519 145 145 0 3514 0
[pid=24012] vsize: 14636
Current children cumulated CPU time (s) 79.65
Current children cumulated vsize (Kb) 16760

[startup+90.0109 s]
Raw data (loadavg): 0.98 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3566 0 0 0 8945 19 0 0 25 0 1 0 1796353815 14987264 3519 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 3659 3519 145 145 0 3514 0
[pid=24012] vsize: 14636
Current children cumulated CPU time (s) 89.66
Current children cumulated vsize (Kb) 16760

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3821 0 0 0 9941 20 0 0 25 0 1 0 1796353815 16035840 3774 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 3915 3774 145 145 0 3770 0
[pid=24012] vsize: 15660
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 17784

[startup+110.012 s]
Raw data (loadavg): 0.98 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4170 0 0 0 10935 23 0 0 25 0 1 0 1796353815 17461248 4123 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 4263 4123 145 145 0 4118 0
[pid=24012] vsize: 17052
Current children cumulated CPU time (s) 109.6
Current children cumulated vsize (Kb) 19176

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4581 0 0 0 11928 25 0 0 25 0 1 0 1796353815 19132416 4534 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 4671 4534 145 145 0 4526 0
[pid=24012] vsize: 18684
Current children cumulated CPU time (s) 119.55
Current children cumulated vsize (Kb) 20808

[startup+130.013 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4663 0 0 0 12927 26 0 0 25 0 1 0 1796353815 19460096 4616 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 4751 4616 145 145 0 4606 0
[pid=24012] vsize: 19004
Current children cumulated CPU time (s) 129.55
Current children cumulated vsize (Kb) 21128

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4663 0 0 0 13927 26 0 0 25 0 1 0 1796353815 19460096 4616 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 4751 4616 145 145 0 4606 0
[pid=24012] vsize: 19004
Current children cumulated CPU time (s) 139.55
Current children cumulated vsize (Kb) 21128

[startup+150.014 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4663 0 0 0 14927 26 0 0 25 0 1 0 1796353815 19460096 4616 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 4751 4616 145 145 0 4606 0
[pid=24012] vsize: 19004
Current children cumulated CPU time (s) 149.55
Current children cumulated vsize (Kb) 21128

[startup+160.015 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4663 0 0 0 15927 26 0 0 25 0 1 0 1796353815 19460096 4616 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 4751 4616 145 145 0 4606 0
[pid=24012] vsize: 19004
Current children cumulated CPU time (s) 159.55
Current children cumulated vsize (Kb) 21128

[startup+170.016 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5076 0 0 0 16921 29 0 0 25 0 1 0 1796353815 21151744 5029 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 5164 5029 145 145 0 5019 0
[pid=24012] vsize: 20656
Current children cumulated CPU time (s) 169.52
Current children cumulated vsize (Kb) 22780

[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5534 0 0 0 17912 33 0 0 25 0 1 0 1796353815 23003136 5487 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 5616 5487 145 145 0 5471 0
[pid=24012] vsize: 22464
Current children cumulated CPU time (s) 179.47
Current children cumulated vsize (Kb) 24588

[startup+190.017 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5676 0 0 0 18909 34 0 0 25 0 1 0 1796353815 23580672 5629 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 5757 5629 145 145 0 5612 0
[pid=24012] vsize: 23028
Current children cumulated CPU time (s) 189.45
Current children cumulated vsize (Kb) 25152

[startup+200.018 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5676 0 0 0 19910 34 0 0 25 0 1 0 1796353815 23580672 5629 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 5757 5629 145 145 0 5612 0
[pid=24012] vsize: 23028
Current children cumulated CPU time (s) 199.46
Current children cumulated vsize (Kb) 25152

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5676 0 0 0 20910 34 0 0 25 0 1 0 1796353815 23580672 5629 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 5757 5629 145 145 0 5612 0
[pid=24012] vsize: 23028
Current children cumulated CPU time (s) 209.46
Current children cumulated vsize (Kb) 25152

[startup+220.02 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5676 0 0 0 21910 34 0 0 25 0 1 0 1796353815 23580672 5629 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 5757 5629 145 145 0 5612 0
[pid=24012] vsize: 23028
Current children cumulated CPU time (s) 219.46
Current children cumulated vsize (Kb) 25152

[startup+230.019 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 6013 0 0 0 22904 36 0 0 25 0 1 0 1796353815 24961024 5966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 6094 5966 145 145 0 5949 0
[pid=24012] vsize: 24376
Current children cumulated CPU time (s) 229.42
Current children cumulated vsize (Kb) 26500

[startup+240.02 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 6501 0 0 0 23896 40 0 0 25 0 1 0 1796353815 26959872 6454 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 6582 6454 145 145 0 6437 0
[pid=24012] vsize: 26328
Current children cumulated CPU time (s) 239.38
Current children cumulated vsize (Kb) 28452

[startup+250.021 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 24886 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134558147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0
[pid=24012] vsize: 28584
Current children cumulated CPU time (s) 249.32
Current children cumulated vsize (Kb) 30708

[startup+260.022 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 25886 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0
[pid=24012] vsize: 28584
Current children cumulated CPU time (s) 259.32
Current children cumulated vsize (Kb) 30708

[startup+270.022 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 26886 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0
[pid=24012] vsize: 28584
Current children cumulated CPU time (s) 269.32
Current children cumulated vsize (Kb) 30708

[startup+280.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 27887 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0
[pid=24012] vsize: 28584
Current children cumulated CPU time (s) 279.33
Current children cumulated vsize (Kb) 30708

[startup+290.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 28887 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0
[pid=24012] vsize: 28584
Current children cumulated CPU time (s) 289.33
Current children cumulated vsize (Kb) 30708

[startup+300.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 29887 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223104 134555544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0
[pid=24012] vsize: 28584
Current children cumulated CPU time (s) 299.33
Current children cumulated vsize (Kb) 30708

[startup+310.026 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7069 0 0 0 30888 44 0 0 25 0 1 0 1796353815 29532160 7022 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7022 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 309.34
Current children cumulated vsize (Kb) 30964

[startup+320.027 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 31888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 319.34
Current children cumulated vsize (Kb) 30964

[startup+330.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 32888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 329.34
Current children cumulated vsize (Kb) 30964

[startup+340.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 33888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 339.34
Current children cumulated vsize (Kb) 30964

[startup+350.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 34888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 349.34
Current children cumulated vsize (Kb) 30964

[startup+360.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 35888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 359.34
Current children cumulated vsize (Kb) 30964

[startup+370.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 36889 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 369.35
Current children cumulated vsize (Kb) 30964

[startup+380.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 37889 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 379.35
Current children cumulated vsize (Kb) 30964

[startup+390.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 38889 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223104 134556205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 389.35
Current children cumulated vsize (Kb) 30964

[startup+400.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 39890 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 399.36
Current children cumulated vsize (Kb) 30964

[startup+410.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 40890 45 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0
[pid=24012] vsize: 28840
Current children cumulated CPU time (s) 409.37
Current children cumulated vsize (Kb) 30964

[startup+420.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7142 0 0 0 41888 45 0 0 25 0 1 0 1796353815 29827072 7095 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7282 7095 145 145 0 7137 0
[pid=24012] vsize: 29128
Current children cumulated CPU time (s) 419.35
Current children cumulated vsize (Kb) 31252

[startup+430.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7418 0 0 0 42884 47 0 0 25 0 1 0 1796353815 30982144 7371 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7564 7371 145 145 0 7419 0
[pid=24012] vsize: 30256
Current children cumulated CPU time (s) 429.33
Current children cumulated vsize (Kb) 32380

[startup+440.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7670 0 0 0 43879 50 0 0 25 0 1 0 1796353815 32026624 7623 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 7819 7623 145 145 0 7674 0
[pid=24012] vsize: 31276
Current children cumulated CPU time (s) 439.31
Current children cumulated vsize (Kb) 33400

[startup+450.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7909 0 0 0 44875 52 0 0 25 0 1 0 1796353815 33001472 7862 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8057 7862 145 145 0 7912 0
[pid=24012] vsize: 32228
Current children cumulated CPU time (s) 449.29
Current children cumulated vsize (Kb) 34352

[startup+460.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7998 0 0 0 45874 53 0 0 25 0 1 0 1796353815 33366016 7951 4294967295 134512640 135094434 3221224432 3221223024 134557277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8146 7951 145 145 0 8001 0
[pid=24012] vsize: 32584
Current children cumulated CPU time (s) 459.29
Current children cumulated vsize (Kb) 34708

[startup+470.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7998 0 0 0 46873 53 0 0 25 0 1 0 1796353815 33366016 7951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8146 7951 145 145 0 8001 0
[pid=24012] vsize: 32584
Current children cumulated CPU time (s) 469.28
Current children cumulated vsize (Kb) 34708

[startup+480.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7998 0 0 0 47873 53 0 0 25 0 1 0 1796353815 33366016 7951 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8146 7951 145 145 0 8001 0
[pid=24012] vsize: 32584
Current children cumulated CPU time (s) 479.28
Current children cumulated vsize (Kb) 34708

[startup+490.039 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8003 0 0 0 48874 53 0 0 25 0 1 0 1796353815 33394688 7956 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8153 7956 145 145 0 8008 0
[pid=24012] vsize: 32612
Current children cumulated CPU time (s) 489.29
Current children cumulated vsize (Kb) 34736

[startup+500.039 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8011 0 0 0 49873 54 0 0 25 0 1 0 1796353815 33427456 7964 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8161 7964 145 145 0 8016 0
[pid=24012] vsize: 32644
Current children cumulated CPU time (s) 499.29
Current children cumulated vsize (Kb) 34768

[startup+510.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8015 0 0 0 50872 54 0 0 25 0 1 0 1796353815 33443840 7968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24012/statm): 8165 7968 145 145 0 8020 0
[pid=24012] vsize: 32660
Current children cumulated CPU time (s) 509.28
Current children cumulated vsize (Kb) 34784

[startup+520.041 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8015 0 0 0 51872 54 0 0 25 0 1 0 1796353815 33443840 7968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8165 7968 145 145 0 8020 0
[pid=24012] vsize: 32660
Current children cumulated CPU time (s) 519.28
Current children cumulated vsize (Kb) 34784

[startup+530.042 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8015 0 0 0 52872 54 0 0 25 0 1 0 1796353815 33443840 7968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8165 7968 145 145 0 8020 0
[pid=24012] vsize: 32660
Current children cumulated CPU time (s) 529.28
Current children cumulated vsize (Kb) 34784

[startup+540.042 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8021 0 0 0 53872 54 0 0 25 0 1 0 1796353815 33476608 7974 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8173 7974 145 145 0 8028 0
[pid=24012] vsize: 32692
Current children cumulated CPU time (s) 539.28
Current children cumulated vsize (Kb) 34816

[startup+550.043 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8021 0 0 0 54872 55 0 0 25 0 1 0 1796353815 33476608 7974 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8173 7974 145 145 0 8028 0
[pid=24012] vsize: 32692
Current children cumulated CPU time (s) 549.29
Current children cumulated vsize (Kb) 34816

[startup+560.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8026 0 0 0 55873 55 0 0 25 0 1 0 1796353815 33492992 7979 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8177 7979 145 145 0 8032 0
[pid=24012] vsize: 32708
Current children cumulated CPU time (s) 559.3
Current children cumulated vsize (Kb) 34832

[startup+570.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8040 0 0 0 56873 55 0 0 25 0 1 0 1796353815 33542144 7993 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8189 7993 145 145 0 8044 0
[pid=24012] vsize: 32756
Current children cumulated CPU time (s) 569.3
Current children cumulated vsize (Kb) 34880

[startup+580.046 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8109 0 0 0 57872 56 0 0 25 0 1 0 1796353815 33816576 8062 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8256 8062 145 145 0 8111 0
[pid=24012] vsize: 33024
Current children cumulated CPU time (s) 579.3
Current children cumulated vsize (Kb) 35148

[startup+590.047 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8110 0 0 0 58872 56 0 0 25 0 1 0 1796353815 33816576 8063 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8256 8063 145 145 0 8111 0
[pid=24012] vsize: 33024
Current children cumulated CPU time (s) 589.3
Current children cumulated vsize (Kb) 35148

[startup+600.048 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8110 0 0 0 59872 56 0 0 25 0 1 0 1796353815 33816576 8063 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8256 8063 145 145 0 8111 0
[pid=24012] vsize: 33024
Current children cumulated CPU time (s) 599.3
Current children cumulated vsize (Kb) 35148

[startup+610.048 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8110 0 0 0 60872 56 0 0 25 0 1 0 1796353815 33816576 8063 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8256 8063 145 145 0 8111 0
[pid=24012] vsize: 33024
Current children cumulated CPU time (s) 609.3
Current children cumulated vsize (Kb) 35148

[startup+620.049 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8111 0 0 0 61872 56 0 0 25 0 1 0 1796353815 33816576 8064 4294967295 134512640 135094434 3221224432 3221223104 134555583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8256 8064 145 145 0 8111 0
[pid=24012] vsize: 33024
Current children cumulated CPU time (s) 619.3
Current children cumulated vsize (Kb) 35148

[startup+630.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8111 0 0 0 62873 56 0 0 25 0 1 0 1796353815 33816576 8064 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8256 8064 145 145 0 8111 0
[pid=24012] vsize: 33024
Current children cumulated CPU time (s) 629.31
Current children cumulated vsize (Kb) 35148

[startup+640.051 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8119 0 0 0 63873 56 0 0 25 0 1 0 1796353815 33873920 8072 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8270 8072 145 145 0 8125 0
[pid=24012] vsize: 33080
Current children cumulated CPU time (s) 639.31
Current children cumulated vsize (Kb) 35204

[startup+650.051 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8119 0 0 0 64873 56 0 0 25 0 1 0 1796353815 33873920 8072 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8270 8072 145 145 0 8125 0
[pid=24012] vsize: 33080
Current children cumulated CPU time (s) 649.31
Current children cumulated vsize (Kb) 35204

[startup+660.053 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8119 0 0 0 65873 56 0 0 25 0 1 0 1796353815 33873920 8072 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8270 8072 145 145 0 8125 0
[pid=24012] vsize: 33080
Current children cumulated CPU time (s) 659.31
Current children cumulated vsize (Kb) 35204

[startup+670.054 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8119 0 0 0 66874 56 0 0 25 0 1 0 1796353815 33873920 8072 4294967295 134512640 135094434 3221224432 3221222944 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8270 8072 145 145 0 8125 0
[pid=24012] vsize: 33080
Current children cumulated CPU time (s) 669.32
Current children cumulated vsize (Kb) 35204

[startup+680.055 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8125 0 0 0 67874 56 0 0 25 0 1 0 1796353815 33906688 8078 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8278 8078 145 145 0 8133 0
[pid=24012] vsize: 33112
Current children cumulated CPU time (s) 679.32
Current children cumulated vsize (Kb) 35236

[startup+690.055 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8126 0 0 0 68874 56 0 0 25 0 1 0 1796353815 33906688 8079 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8278 8079 145 145 0 8133 0
[pid=24012] vsize: 33112
Current children cumulated CPU time (s) 689.32
Current children cumulated vsize (Kb) 35236

[startup+700.056 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8200 0 0 0 69873 57 0 0 25 0 1 0 1796353815 34234368 8153 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8358 8153 145 145 0 8213 0
[pid=24012] vsize: 33432
Current children cumulated CPU time (s) 699.32
Current children cumulated vsize (Kb) 35556

[startup+710.057 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 70870 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0
[pid=24012] vsize: 34064
Current children cumulated CPU time (s) 709.3
Current children cumulated vsize (Kb) 36188

[startup+720.058 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 71870 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0
[pid=24012] vsize: 34064
Current children cumulated CPU time (s) 719.3
Current children cumulated vsize (Kb) 36188

[startup+730.058 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 72870 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0
[pid=24012] vsize: 34064
Current children cumulated CPU time (s) 729.3
Current children cumulated vsize (Kb) 36188

[startup+740.059 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 73871 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223104 134556246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0
[pid=24012] vsize: 34064
Current children cumulated CPU time (s) 739.31
Current children cumulated vsize (Kb) 36188

[startup+750.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 74871 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0
[pid=24012] vsize: 34064
Current children cumulated CPU time (s) 749.31
Current children cumulated vsize (Kb) 36188

[startup+760.062 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8367 0 0 0 75871 58 0 0 25 0 1 0 1796353815 34947072 8320 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8532 8320 145 145 0 8387 0
[pid=24012] vsize: 34128
Current children cumulated CPU time (s) 759.31
Current children cumulated vsize (Kb) 36252

[startup+770.062 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8368 0 0 0 76871 58 0 0 25 0 1 0 1796353815 34947072 8321 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8532 8321 145 145 0 8387 0
[pid=24012] vsize: 34128
Current children cumulated CPU time (s) 769.31
Current children cumulated vsize (Kb) 36252

[startup+780.062 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8368 0 0 0 77871 58 0 0 25 0 1 0 1796353815 34947072 8321 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8532 8321 145 145 0 8387 0
[pid=24012] vsize: 34128
Current children cumulated CPU time (s) 779.31
Current children cumulated vsize (Kb) 36252

[startup+790.063 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8368 0 0 0 78872 58 0 0 25 0 1 0 1796353815 34947072 8321 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8532 8321 145 145 0 8387 0
[pid=24012] vsize: 34128
Current children cumulated CPU time (s) 789.32
Current children cumulated vsize (Kb) 36252

[startup+800.064 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8373 0 0 0 79870 59 0 0 25 0 1 0 1796353815 34979840 8326 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24012/statm): 8540 8326 145 145 0 8395 0
[pid=24012] vsize: 34160
Current children cumulated CPU time (s) 799.31
Current children cumulated vsize (Kb) 36284

[startup+810.064 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8378 0 0 0 80870 59 0 0 25 0 1 0 1796353815 35012608 8331 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8548 8331 145 145 0 8403 0
[pid=24012] vsize: 34192
Current children cumulated CPU time (s) 809.31
Current children cumulated vsize (Kb) 36316

[startup+820.065 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8383 0 0 0 81870 59 0 0 25 0 1 0 1796353815 35012608 8336 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8548 8336 145 145 0 8403 0
[pid=24012] vsize: 34192
Current children cumulated CPU time (s) 819.31
Current children cumulated vsize (Kb) 36316

[startup+830.066 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8502 0 0 0 82868 60 0 0 25 0 1 0 1796353815 35483648 8455 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8663 8455 145 145 0 8518 0
[pid=24012] vsize: 34652
Current children cumulated CPU time (s) 829.3
Current children cumulated vsize (Kb) 36776

[startup+840.066 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 83868 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 839.3
Current children cumulated vsize (Kb) 36780

[startup+850.067 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 84868 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 849.3
Current children cumulated vsize (Kb) 36780

[startup+860.069 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 85869 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 859.31
Current children cumulated vsize (Kb) 36780

[startup+870.07 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 86869 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 869.31
Current children cumulated vsize (Kb) 36780

[startup+880.07 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 87869 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 879.31
Current children cumulated vsize (Kb) 36780

[startup+890.071 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 88869 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 889.31
Current children cumulated vsize (Kb) 36780

[startup+900.072 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 89870 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 899.32
Current children cumulated vsize (Kb) 36780

[startup+910.073 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 90870 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 909.32
Current children cumulated vsize (Kb) 36780

[startup+920.073 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 91870 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0
[pid=24012] vsize: 34656
Current children cumulated CPU time (s) 919.32
Current children cumulated vsize (Kb) 36780

[startup+930.074 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8763 0 0 0 92865 62 0 0 25 0 1 0 1796353815 36569088 8716 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 8928 8716 145 145 0 8783 0
[pid=24012] vsize: 35712
Current children cumulated CPU time (s) 929.29
Current children cumulated vsize (Kb) 37836

[startup+940.075 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9075 0 0 0 93859 65 0 0 25 0 1 0 1796353815 37871616 9028 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9246 9028 145 145 0 9101 0
[pid=24012] vsize: 36984
Current children cumulated CPU time (s) 939.26
Current children cumulated vsize (Kb) 39108

[startup+950.076 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9371 0 0 0 94855 67 0 0 25 0 1 0 1796353815 39108608 9324 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9548 9324 145 145 0 9403 0
[pid=24012] vsize: 38192
Current children cumulated CPU time (s) 949.24
Current children cumulated vsize (Kb) 40316

[startup+960.077 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9668 0 0 0 95851 68 0 0 25 0 1 0 1796353815 40378368 9621 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9858 9621 145 145 0 9713 0
[pid=24012] vsize: 39432
Current children cumulated CPU time (s) 959.21
Current children cumulated vsize (Kb) 41556

[startup+970.078 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9755 0 0 0 96850 69 0 0 25 0 1 0 1796353815 40730624 9708 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9708 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 969.21
Current children cumulated vsize (Kb) 41900

[startup+980.079 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9755 0 0 0 97850 69 0 0 25 0 1 0 1796353815 40730624 9708 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9708 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 979.21
Current children cumulated vsize (Kb) 41900

[startup+990.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9756 0 0 0 98850 69 0 0 25 0 1 0 1796353815 40730624 9709 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9709 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 989.21
Current children cumulated vsize (Kb) 41900

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9757 0 0 0 99850 69 0 0 25 0 1 0 1796353815 40730624 9710 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9710 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 999.21
Current children cumulated vsize (Kb) 41900

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9757 0 0 0 100850 69 0 0 25 0 1 0 1796353815 40730624 9710 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9710 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1009.21
Current children cumulated vsize (Kb) 41900

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9757 0 0 0 101851 69 0 0 25 0 1 0 1796353815 40730624 9710 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9710 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1019.22
Current children cumulated vsize (Kb) 41900

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 102850 70 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1029.22
Current children cumulated vsize (Kb) 41900

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 103849 71 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1039.22
Current children cumulated vsize (Kb) 41900

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 104849 71 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1049.22
Current children cumulated vsize (Kb) 41900

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 105849 71 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1059.22
Current children cumulated vsize (Kb) 41900

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 106849 71 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1069.22
Current children cumulated vsize (Kb) 41900

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 107849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1079.23
Current children cumulated vsize (Kb) 41900

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 108849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1089.23
Current children cumulated vsize (Kb) 41900

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 109849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1099.23
Current children cumulated vsize (Kb) 41900

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 110849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1109.23
Current children cumulated vsize (Kb) 41900

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 111849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1119.23
Current children cumulated vsize (Kb) 41900

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 112850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1129.24
Current children cumulated vsize (Kb) 41900

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 113850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1139.24
Current children cumulated vsize (Kb) 41900

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 114850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1149.24
Current children cumulated vsize (Kb) 41900

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 115850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1159.24
Current children cumulated vsize (Kb) 41900

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 116850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1169.24
Current children cumulated vsize (Kb) 41900

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 117850 73 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1179.25
Current children cumulated vsize (Kb) 41900

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9759 0 0 0 118850 73 0 0 25 0 1 0 1796353815 40730624 9712 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9712 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1189.25
Current children cumulated vsize (Kb) 41900

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9759 0 0 0 119850 73 0 0 25 0 1 0 1796353815 40730624 9712 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9712 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1199.25
Current children cumulated vsize (Kb) 41900

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9759 0 0 0 120851 73 0 0 25 0 1 0 1796353815 40730624 9712 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9712 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1209.26
Current children cumulated vsize (Kb) 41900



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.98 2/57 24012
Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24008/statm): 531 226 485 147 0 384 0
[pid=24008] vsize: 2124
Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9759 0 0 0 120851 73 0 0 25 0 1 0 1796353815 40730624 9712 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24012/statm): 9944 9712 145 145 0 9799 0
[pid=24012] vsize: 39776
Current children cumulated CPU time (s) 1209.26
Current children cumulated vsize (Kb) 41900

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.27
CPU user time (s): 1208.51
CPU system time (s): 0.754885
CPU usage (%): 99.9292
Max. virtual memory (cumulated for all children) (Kb): 41900

Verifier Data

ERROR: no interpretation found !