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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-misc07.opb
MD5SUM	54df16ee65da54d5975ffedee80d2bb9
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1408128
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11486079
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	280
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	253
Trace number 31219

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-05-25 23:09:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22614 boxname=wulflinc11 idbench=1430 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  54df16ee65da54d5975ffedee80d2bb9  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 22614
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        824536 kB
Buffers:          6968 kB
Cached:         183640 kB
SwapCached:        948 kB
Active:          33444 kB
Inactive:       159344 kB
HighTotal:      131008 kB
HighFree:         8372 kB
LowTotal:       903652 kB
LowFree:        816164 kB
SwapTotal:     2097136 kB
SwapFree:      2095364 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5032 kB
Slab:            11496 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:29:45 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 22614 7 1229.84 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 243]---> BDD-cost:   51
c ---[ 241]---> BDD-cost:   51
c ---[ 239]---> BDD-cost:   51
c ---[ 237]---> BDD-cost:   51
c ---[ 235]---> BDD-cost:   51
c ---[ 233]---> BDD-cost:   51
c ---[ 231]---> BDD-cost:   51
c ---[ 230]---> BDD-cost:  239
c ---[ 229]---> BDD-cost:  239
c ---[ 228]---> BDD-cost:  239
c ---[  99]---> Sorter-cost:  127     Base:
c ---[  97]---> Sorter-cost:  127     Base:
c ---[  95]---> Sorter-cost:  127     Base:
c ---[  93]---> Sorter-cost:  127     Base:
c ---[  91]---> Sorter-cost:  127     Base:
c ---[  89]---> Sorter-cost:  127     Base:
c ---[  87]---> Sorter-cost:  127     Base:
c ---[  85]---> Sorter-cost:  127     Base:
c ---[  83]---> Sorter-cost:  127     Base:
c ---[  81]---> Sorter-cost:  127     Base:
c ---[  79]---> Sorter-cost:  127     Base:
c ---[  77]---> Sorter-cost:  127     Base:
c ---[  75]---> Sorter-cost:  127     Base:
c ---[  73]---> Sorter-cost:  127     Base:
c ---[  71]---> Sorter-cost:  127     Base:
c ---[  69]---> Sorter-cost:  127     Base:
c ---[  67]---> Sorter-cost:  127     Base:
c ---[  65]---> Sorter-cost:  127     Base:
c ---[  63]---> Sorter-cost:  127     Base:
c ---[  61]---> Sorter-cost:  127     Base:
c ---[  59]---> Sorter-cost:  127     Base:
c ---[  57]---> Sorter-cost:  127     Base:
c ---[  55]---> Sorter-cost:  127     Base:
c ---[  53]---> Sorter-cost:  127     Base:
c ---[  51]---> Sorter-cost:  127     Base:
c ---[  49]---> Sorter-cost:  127     Base:
c ---[  47]---> Sorter-cost:  127     Base:
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  33]---> BDD-cost:   50
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   48
c ---[  28]---> BDD-cost:   48
c ---[  27]---> BDD-cost:   48
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   50
c ---[  22]---> BDD-cost:   50
c ---[  21]---> BDD-cost:   50
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   48
c ---[  16]---> BDD-cost:   48
c ---[  15]---> BDD-cost:   48
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   50
c ---[  10]---> BDD-cost:   50
c ---[   9]---> BDD-cost:   50
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:   48
c ---[   3]---> BDD-cost:   48
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25782    84321 |    8594       0        0     nan |  0.000 % |
c |       104 |   25782    84321 |    9453     104     6117    58.8 |  2.677 % |
c ==============================================================================
c [1mFound solution: 1611648[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       123 |   25795    84354 |    8598     123     6748    54.9 |  2.677 % |
c ==============================================================================
c [1mFound solution: 1508608[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       125 |   25808    84385 |    8602     125     6762    54.1 |  2.677 % |
c |       226 |   25808    84385 |    9462     226    17913    79.3 |  2.700 % |
c |       376 |   25808    84385 |   10408     376    23984    63.8 |  2.700 % |
c |       602 |   25808    84385 |   11449     602    49428    82.1 |  2.700 % |
c |       939 |   25787    84310 |   12594     937    66619    71.1 |  2.715 % |
c |      1446 |   25787    84310 |   13853    1444   118779    82.3 |  2.715 % |
c |      2206 |   25732    84151 |   15238    2192   175466    80.0 |  2.845 % |
c ==============================================================================
c [1mFound solution: 1476608[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2813 |   25675    84026 |    8558    2786   202362    72.6 |  2.845 % |
c |      2914 |   25675    84026 |    9413    2887   216333    74.9 |  3.131 % |
c |      3064 |   25675    84026 |   10355    3037   232590    76.6 |  3.131 % |
c |      3290 |   25651    83953 |   11390    3260   236544    72.6 |  3.189 % |
c |      3628 |   25623    83890 |   12529    3595   279647    77.8 |  3.290 % |
c |      4136 |   25623    83890 |   13782    4103   311959    76.0 |  3.290 % |
c |      4896 |   25623    83890 |   15161    4863   391121    80.4 |  3.290 % |
c |      6037 |   25623    83890 |   16677    6004   489351    81.5 |  3.290 % |
c |      7749 |   25574    83745 |   18344    7708   650986    84.5 |  3.391 % |
c ==============================================================================
c [1mFound solution: 1470848[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8367 |   25534    83606 |    8511    8319   709343    85.3 |  3.391 % |
c |      8467 |   25513    83531 |    9362    8416   712125    84.6 |  3.502 % |
c |      8618 |   25513    83531 |   10298    8567   720411    84.1 |  3.502 % |
c |      8846 |   25513    83531 |   11328    8795   739938    84.1 |  3.502 % |
c |      9183 |   25513    83531 |   12460    9132   783046    85.7 |  3.502 % |
c |      9690 |   25400    83151 |   13707    9625   842609    87.5 |  3.675 % |
c ==============================================================================
c [1mFound solution: 1465728[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10436 |   25402    83160 |    8467   10369   916955    88.4 |  3.675 % |
c |     10536 |   25402    83160 |    9313    5285   386079    73.1 |  3.729 % |
c |     10686 |   25361    83069 |   10245    5426   393377    72.5 |  3.902 % |
c |     10911 |   25361    83069 |   11269    5651   409599    72.5 |  3.902 % |
c |     11249 |   25361    83069 |   12396    5989   450093    75.2 |  3.902 % |
c |     11755 |   25328    82952 |   13636    6486   476029    73.4 |  3.930 % |
c |     12517 |   25328    82952 |   14999    7248   532015    73.4 |  3.930 % |
c |     13656 |   25328    82952 |   16499    8387   624983    74.5 |  3.930 % |
c |     15365 |   25328    82952 |   18149   10096   891959    88.3 |  3.930 % |
c |     17927 |   25321    82937 |   19964   12657  1137466    89.9 |  3.959 % |
c ==============================================================================
c [1mFound solution: 1459328[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18442 |   25337    82974 |    8445   13172  1195556    90.8 |  3.959 % |
c |     18544 |   25337    82974 |    9289    6688   584306    87.4 |  3.969 % |
c |     18698 |   25337    82974 |   10218    6842   607049    88.7 |  3.969 % |
c |     18923 |   25232    82626 |   11240    7056   627855    89.0 |  4.170 % |
c |     19263 |   25187    82494 |   12364    7389   652013    88.2 |  4.285 % |
c |     19770 |   25170    82456 |   13600    7895   721465    91.4 |  4.357 % |
c |     20529 |   25170    82456 |   14960    8654   806216    93.2 |  4.357 % |
c |     21671 |   25127    82305 |   16456    9793   890194    90.9 |  4.443 % |
c ==============================================================================
c [1mFound solution: 1440128[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22665 |   25125    82307 |    8375   10784  1014528    94.1 |  4.443 % |
c |     22765 |   25125    82307 |    9212    5492   368580    67.1 |  4.497 % |
c |     22916 |   25125    82307 |   10133    5643   371798    65.9 |  4.497 % |
c |     23143 |   25114    82283 |   11147    5869   407568    69.4 |  4.540 % |
c |     23480 |   25114    82283 |   12261    6206   427989    69.0 |  4.540 % |
c ==============================================================================
c [1mFound solution: 1429248[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23792 |   25125    82313 |    8375    6518   470528    72.2 |  4.540 % |
c |     23896 |   25125    82313 |    9212    6622   482346    72.8 |  4.550 % |
c |     24046 |   25044    82051 |   10133    6765   493619    73.0 |  4.722 % |
c |     24274 |   24863    81448 |   11147    6973   507046    72.7 |  5.038 % |
c |     24613 |   24844    81404 |   12261    7307   529616    72.5 |  5.110 % |
c |     25119 |   24844    81404 |   13488    7813   610135    78.1 |  5.110 % |
c |     25880 |   24844    81404 |   14836    8574   646861    75.4 |  5.110 % |
c |     27022 |   24824    81360 |   16320    9711   732271    75.4 |  5.196 % |
c |     28734 |   24824    81360 |   17952   11423   891715    78.1 |  5.196 % |
c |     31297 |   24824    81360 |   19747   13986  1292109    92.4 |  5.196 % |
c |     35141 |   24802    81312 |   21722   17826  1712988    96.1 |  5.282 % |
c |     40907 |   24784    81273 |   23894   23589  2293176    97.2 |  5.354 % |
c |     49556 |   24773    81249 |   26284   20011  2092469   104.6 |  5.397 % |
c |     62530 |   24740    81132 |   28912   19252  1361391    70.7 |  5.426 % |
c |     81991 |   24660    80889 |   31804   23203  1916008    82.6 |  5.641 % |
c ==============================================================================
c [1mFound solution: 1419008[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86665 |   24652    80876 |    8217   27873  2312061    82.9 |  5.641 % |
c |     86765 |   24652    80876 |    9038    7069   359139    50.8 |  5.734 % |
c |     86915 |   24589    80694 |    9942    7212   361365    50.1 |  5.906 % |
c |     87140 |   24589    80694 |   10936    7437   379936    51.1 |  5.906 % |
c |     87478 |   24543    80590 |   12030    7770   392965    50.6 |  6.121 % |
c |     87985 |   24543    80590 |   13233    8277   449311    54.3 |  6.121 % |
c |     88744 |   24543    80590 |   14556    9036   528727    58.5 |  6.121 % |
c |     89885 |   24543    80590 |   16012   10177   658551    64.7 |  6.121 % |
c |     91595 |   24543    80590 |   17613   11887   865744    72.8 |  6.121 % |
c |     94157 |   24493    80427 |   19375   14439  1148273    79.5 |  6.221 % |
c |     98002 |   24449    80290 |   21312   18275  1436698    78.6 |  6.322 % |
c |    103768 |   24432    80252 |   23444   12999   898365    69.1 |  6.393 % |
c |    112417 |   24421    80228 |   25788   21646  1813298    83.8 |  6.436 % |
c |    125391 |   24421    80228 |   28367   20828  1681241    80.7 |  6.436 % |
c |    144852 |   24406    80175 |   31204   24623  2133182    86.6 |  6.451 % |
c ==============================================================================
c [1mFound solution: 1415168[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    162569 |   24351    80012 |    8117   23650  2252373    95.2 |  6.451 % |
c |    162670 |   24351    80012 |    8928    6014   408136    67.9 |  6.645 % |
c |    162820 |   24351    80012 |    9821    6164   422946    68.6 |  6.645 % |
c |    163045 |   24351    80012 |   10803    6389   443258    69.4 |  6.645 % |
c |    163382 |   24351    80012 |   11884    6726   487694    72.5 |  6.645 % |
c |    163888 |   24351    80012 |   13072    7232   518741    71.7 |  6.645 % |
c |    164651 |   24338    79983 |   14379    7993   606780    75.9 |  6.702 % |
c |    165792 |   24338    79983 |   15817    9134   770652    84.4 |  6.702 % |
c |    167500 |   24338    79983 |   17399   10842   883396    81.5 |  6.702 % |
c |    170062 |   24329    79952 |   19139   13401  1257807    93.9 |  6.716 % |
c |    173906 |   24318    79928 |   21053   17243  1583558    91.8 |  6.759 % |
c |    179672 |   24318    79928 |   23158   11574   882126    76.2 |  6.759 % |
c |    188322 |   24318    79928 |   25474   20224  1960555    96.9 |  6.759 % |
c |    201298 |   24296    79880 |   28022   20015  1816864    90.8 |  6.845 % |
c ==============================================================================
c [1mFound solution: 1408128[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    209149 |   24306    79907 |    8102   27866  2723490    97.7 |  6.845 % |
c |    209250 |   24306    79907 |    8912    7068   466379    66.0 |  6.853 % |
c |    209401 |   24306    79907 |    9803    7219   479276    66.4 |  6.853 % |
c |    209627 |   24306    79907 |   10783    7445   508961    68.4 |  6.853 % |
c |    209967 |   24306    79907 |   11862    7785   532660    68.4 |  6.853 % |
c |    210473 |   24306    79907 |   13048    8291   602654    72.7 |  6.853 % |
c |    211232 |   24241    79734 |   14353    9039   675578    74.7 |  7.067 % |
c |    212372 |   24241    79734 |   15788   10179   812871    79.9 |  7.067 % |
c |    214080 |   24230    79710 |   17367   11884   928908    78.2 |  7.110 % |
c |    216643 |   24224    79690 |   19104   14443  1193339    82.6 |  7.124 % |
c |    220487 |   24224    79690 |   21014   18287  1514845    82.8 |  7.124 % |
c |    226254 |   24224    79690 |   23115   13248  1001035    75.6 |  7.124 % |
c |    234904 |   24224    79690 |   25427   21898  1857367    84.8 |  7.124 % |
c |    247878 |   24201    79627 |   27970   21357  1844939    86.4 |  7.210 % |
c |    267340 |   24011    79030 |   30767   25653  2211361    86.2 |  7.639 % |
c |    296534 |   23994    78992 |   33844   22302  2056277    92.2 |  7.711 % |
c |    340323 |   23969    78936 |   37228   27120  2364139    87.2 |  7.811 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11919 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.97 0.91 2/54 11915
Raw data (stat): 11915 (runsolver) R 11914 25830 25829 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784500568 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.0009 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.0018 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.0023 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.0027 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.0025 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.006 s]
Raw data (loadavg): 1.15 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.007 s]
Raw data (loadavg): 1.12 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.007 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.007 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.007 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.008 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.008 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.007 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.009 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.01 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.009 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.01 s]
Raw data (loadavg): 1.09 1.02 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.011 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.011 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.011 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.011 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.011 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.012 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.012 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.013 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.013 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.013 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.014 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.015 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.7 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 11919
Raw data (stat): 11915 (minisat+_script) S 11914 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784500568 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.7
CPU time (s): 1229.84
CPU user time (s): 1229.51
CPU system time (s): 0.332949
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####