PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare2_1.opb
MD5SUM	a84a96a9314212f3d8ecd5227c500cef
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	91392
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 numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1202.31
Number of variables	330
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	150
Trace number 30909

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-05-25 20:42:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22299 boxname=wulflinc12 idbench=1115 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  a84a96a9314212f3d8ecd5227c500cef  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-markshare2_1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-markshare2_1.opb
IDLAUNCH: 22299
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        328240 kB
Buffers:         34972 kB
Cached:         649972 kB
SwapCached:        564 kB
Active:          60752 kB
Inactive:       626644 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        327988 kB
SwapTotal:     2097136 kB
SwapFree:      2096076 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            13384 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:03:08 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 22299 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN 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 [1mFound solution: 8658716[0m
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 [1mFound solution: 5260062[0m
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 [1mFound solution: 4950048[0m
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 [1mFound solution: 4620607[0m
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 [1mFound solution: 4249759[0m
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 [1mFound solution: 3339853[0m
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 [1mFound solution: 3334229[0m
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 [1mFound solution: 3287413[0m
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 [1mFound solution: 2290547[0m
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 [1mFound solution: 1436307[0m
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 [1mFound solution: 1226125[0m
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 [1mFound solution: 937675[0m
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 [1mFound solution: 681120[0m
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 % |
c |    787828 |   40314   136607 |   46391   14662   767614    52.4 |  6.533 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 16539 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 16535
Raw data (stat): 16535 (runsolver) R 16534 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783617904 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0046 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0047 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0055 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.044 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16539
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.06 s]
Raw data (loadavg): 1.07 0.99 0.91 3/59 16585
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.06 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 16592
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.06 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 16592
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 16592
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 16592
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 16592
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.07 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 16592
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 16594
Raw data (stat): 16535 (minisat+_script) S 16534 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783617904 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.85
CPU user time (s): 1229.42
CPU system time (s): 0.426935
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####