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-markshare1_1.opb
MD5SUM	452acf9ed3adc2d2cfe293dad01c0934
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	167110
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.02
Number of variables	280
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	130
Trace number 20778

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 21:49:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14482 boxname=wulflinc27 idbench=1114 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  452acf9ed3adc2d2cfe293dad01c0934  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-markshare1_1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-markshare1_1.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-markshare1_1.opb
IDLAUNCH: 14482
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        477272 kB
Buffers:         26488 kB
Cached:         507956 kB
SwapCached:        512 kB
Active:          91596 kB
Inactive:       444768 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        477020 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5092 kB
Slab:            15376 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 22:09:42 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 14482 7 1200.28 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> Adder-cost: 662   maxlim: 3510008   bits: 23/22
c ---[   8]---> Adder-cost: 660   maxlim: 3759828   bits: 23/22
c ---[   6]---> Adder-cost: 770   maxlim: 3884662   bits: 23/22
c ---[   4]---> Adder-cost: 500   maxlim: 3402645   bits: 23/22
c ---[   2]---> Adder-cost: 574   maxlim: 3468109   bits: 23/22
c ---[   0]---> Adder-cost: 558   maxlim: 3462997   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25243    89685 |    8414       0        0     nan |  0.000 % |
c |       100 |   25235    89659 |    9255      99      630     6.4 |  7.959 % |
c |       251 |   25227    89633 |   10180     249     2606    10.5 |  7.984 % |
c |       476 |   25227    89633 |   11199     474     5163    10.9 |  7.984 % |
c ==============================================================================
c [1mFound solution: 2823332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1725     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 |       518 |   29992   100869 |    9997     516     5656    11.0 |  7.984 % |
c |       618 |   29992   100869 |   10996     616    14105    22.9 |  5.848 % |
c |       768 |   29992   100869 |   12096     766    17703    23.1 |  5.848 % |
c |       993 |   29984   100843 |   13306     990    21029    21.2 |  5.866 % |
c |      1330 |   29984   100843 |   14636    1327    26779    20.2 |  5.866 % |
c |      1836 |   29944   100717 |   16100    1828    32887    18.0 |  5.971 % |
c |      2597 |   29928   100665 |   17710    2587    51817    20.0 |  6.007 % |
c |      3736 |   29896   100561 |   19481    3722    77386    20.8 |  6.077 % |
c |      5444 |   29822   100378 |   21429    5395   129426    24.0 |  6.394 % |
c ==============================================================================
c [1mFound solution: 1314153[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |      6516 |   29922   100638 |    9974    6467   152969    23.7 |  6.394 % |
c |      6617 |   29922   100638 |   10971    6568   155502    23.7 |  6.388 % |
c |      6767 |   29922   100638 |   12068    6718   158389    23.6 |  6.388 % |
c |      6994 |   29922   100638 |   13275    6945   160367    23.1 |  6.388 % |
c |      7331 |   29922   100638 |   14602    7282   166162    22.8 |  6.388 % |
c |      7839 |   29922   100638 |   16063    7790   176545    22.7 |  6.388 % |
c |      8598 |   29922   100638 |   17669    8549   198868    23.3 |  6.388 % |
c |      9738 |   29922   100638 |   19436    9689   233827    24.1 |  6.388 % |
c |     11447 |   29922   100638 |   21380   11398   315259    27.7 |  6.388 % |
c |     14010 |   29922   100638 |   23518   13961   427538    30.6 |  6.388 % |
c |     17854 |   29922   100638 |   25869   17805   579229    32.5 |  6.388 % |
c |     23623 |   29922   100638 |   28456   23574   807949    34.3 |  6.388 % |
c |     32274 |   29922   100638 |   31302   16209   618745    38.2 |  6.388 % |
c |     45249 |   29922   100638 |   34432   29184  1254062    43.0 |  6.388 % |
c |     64712 |   29922   100638 |   37876   26801  1301156    48.5 |  6.388 % |
c |     93905 |   29922   100638 |   41663   30811  1635571    53.1 |  6.388 % |
c |    137694 |   29922   100638 |   45830   14739  1030778    69.9 |  6.388 % |
c |    203378 |   29878   100541 |   50413   47181  5971370   126.6 |  6.599 % |
c ==============================================================================
c [1mFound solution: 1207558[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |    209188 |   29862   100514 |    9954   17787  1148976    64.6 |  6.599 % |
c |    209289 |   29862   100514 |   10949    8995   279937    31.1 |  6.969 % |
c |    209439 |   29862   100514 |   12044    9145   282676    30.9 |  6.969 % |
c |    209667 |   29862   100514 |   13248    9373   286276    30.5 |  6.969 % |
c |    210004 |   29862   100514 |   14573    9710   297486    30.6 |  6.969 % |
c |    210510 |   29862   100514 |   16031   10216   310933    30.4 |  6.969 % |
c |    211270 |   29862   100514 |   17634   10976   396244    36.1 |  6.969 % |
c |    212409 |   29843   100470 |   19397   12110   424552    35.1 |  7.057 % |
c |    214117 |   29843   100470 |   21337   13818   493114    35.7 |  7.057 % |
c |    216679 |   29843   100470 |   23471   16380   596835    36.4 |  7.057 % |
c |    220524 |   29843   100470 |   25818   20225   804637    39.8 |  7.057 % |
c |    226290 |   29843   100470 |   28399   25991  1086882    41.8 |  7.057 % |
c |    234940 |   29843   100470 |   31239   18708   785823    42.0 |  7.057 % |
c |    247914 |   29837   100456 |   34363   31681  1326933    41.9 |  7.092 % |
c ==============================================================================
c [1mFound solution: 1108608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |    249712 |   29880   100563 |    9960   33479  1583600    47.3 |  7.092 % |
c |    249812 |   29880   100563 |   10956    7105   382399    53.8 |  7.094 % |
c |    249963 |   29880   100563 |   12051    7256   384475    53.0 |  7.094 % |
c |    250189 |   29880   100563 |   13256    7482   389876    52.1 |  7.094 % |
c |    250527 |   29880   100563 |   14582    7820   396280    50.7 |  7.094 % |
c |    251034 |   29880   100563 |   16040    8327   407804    49.0 |  7.094 % |
c |    251794 |   29880   100563 |   17644    9087   429913    47.3 |  7.094 % |
c |    252933 |   29880   100563 |   19409   10226   475579    46.5 |  7.094 % |
c |    254641 |   29880   100563 |   21350   11934   516261    43.3 |  7.094 % |
c |    257203 |   29880   100563 |   23485   14496   600484    41.4 |  7.094 % |
c |    261047 |   29880   100563 |   25833   18340   829338    45.2 |  7.094 % |
c |    266814 |   29880   100563 |   28417   24107  1122253    46.6 |  7.094 % |
c |    275463 |   29880   100563 |   31258   15551   745019    47.9 |  7.094 % |
c ==============================================================================
c [1mFound solution: 1089440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |    276006 |   29913   100648 |    9971   16094   765762    47.6 |  7.094 % |
c |    276108 |   29913   100648 |   10968    8149   446109    54.7 |  7.102 % |
c |    276259 |   29913   100648 |   12064    8300   448530    54.0 |  7.102 % |
c |    276485 |   29913   100648 |   13271    8526   451891    53.0 |  7.102 % |
c |    276823 |   29913   100648 |   14598    8864   457312    51.6 |  7.102 % |
c |    277330 |   29913   100648 |   16058    9371   473299    50.5 |  7.102 % |
c |    278089 |   29913   100648 |   17664   10130   485980    48.0 |  7.102 % |
c |    279228 |   29913   100648 |   19430   11269   515607    45.8 |  7.102 % |
c |    280939 |   29913   100648 |   21373   12980   577654    44.5 |  7.102 % |
c |    283501 |   29913   100648 |   23511   15542   676169    43.5 |  7.102 % |
c |    287345 |   29913   100648 |   25862   19386   889869    45.9 |  7.102 % |
c |    293113 |   29913   100648 |   28448   25154  1167486    46.4 |  7.102 % |
c |    301762 |   29893   100603 |   31293   17589   788670    44.8 |  7.189 % |
c |    314736 |   29893   100603 |   34422   30563  1416122    46.3 |  7.189 % |
c |    334197 |   29893   100603 |   37864   29048  1220337    42.0 |  7.189 % |
c |    363391 |   29849   100486 |   41651   31324  3237071   103.3 |  7.363 % |
c |    407180 |   29841   100460 |   45816   16315  1056543    64.8 |  7.381 % |
c |    472865 |   29816   100401 |   50398   15756   673322    42.7 |  7.521 % |
c |    571393 |   29810   100383 |   55437   37119  2782462    75.0 |  7.538 % |
c ==============================================================================
c [1mFound solution: 1034581[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    577218 |   29782   100271 |    9927   42939  3482353    81.1 |  7.538 % |
c |    577319 |   29754   100206 |   10919    7554   722143    95.6 |  7.958 % |
c |    577469 |   29754   100206 |   12011    7704   724933    94.1 |  7.958 % |
c |    577696 |   29754   100206 |   13212    7931   727940    91.8 |  7.958 % |
c |    578037 |   29754   100206 |   14534    8272   734777    88.8 |  7.958 % |
c |    578543 |   29754   100206 |   15987    8778   748568    85.3 |  7.958 % |
c |    579302 |   29754   100206 |   17586    9537   771547    80.9 |  7.958 % |
c |    580441 |   29754   100206 |   19344   10676   805532    75.5 |  7.958 % |
c |    582149 |   29754   100206 |   21279   12384   875470    70.7 |  7.958 % |
c |    584711 |   29732   100149 |   23407   14944   971743    65.0 |  8.079 % |
c |    588555 |   29732   100149 |   25748   18788  1142877    60.8 |  8.079 % |
c |    594325 |   29732   100149 |   28322   24558  1404940    57.2 |  8.079 % |
c |    602974 |   29732   100149 |   31155   16951   623581    36.8 |  8.079 % |
c |    615948 |   29732   100149 |   34270   29925  1240647    41.5 |  8.079 % |
c |    635410 |   29652    99966 |   37697   27694  1683818    60.8 |  8.462 % |
c |    664602 |   29652    99966 |   41467   29986  1957424    65.3 |  8.462 % |
c |    708392 |   29620    99891 |   45614   14479   564505    39.0 |  8.671 % |
c |    774076 |   29620    99891 |   50175   15971   645487    40.4 |  8.671 % |
#### 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.73 0.94 0.94 2/54 27013
Raw data (stat): 27013 (runsolver) R 27012 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548446009 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.77 0.94 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 1631 0 0 0 995 3 0 0 25 0 1 0 548446009 8208384 1605 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2004 1605 603 41 0 1963 0
vsize: 8016
[startup+20.0011 s]
Raw data (loadavg): 0.81 0.94 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 2270 0 0 0 1992 5 0 0 25 0 1 0 548446009 10924032 2244 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2667 2244 603 41 0 2626 0
vsize: 10668
[startup+30.0014 s]
Raw data (loadavg): 0.83 0.94 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 2300 0 0 0 2992 6 0 0 25 0 1 0 548446009 11059200 2274 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2700 2274 603 41 0 2659 0
vsize: 10800
[startup+40.0022 s]
Raw data (loadavg): 0.86 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 2768 0 0 0 3991 7 0 0 25 0 1 0 548446009 12926976 2742 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3156 2742 603 41 0 3115 0
vsize: 12624
[startup+50.0026 s]
Raw data (loadavg): 0.88 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 2999 0 0 0 4990 8 0 0 25 0 1 0 548446009 13996032 2973 4294967295 134512640 134672761 3221224528 3221223696 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3417 2973 603 41 0 3376 0
vsize: 13668
[startup+60.0118 s]
Raw data (loadavg): 0.90 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3003 0 0 0 5981 8 0 0 25 0 1 0 548446009 13996032 2977 4294967295 134512640 134672761 3221224528 3221223696 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3417 2977 603 41 0 3376 0
vsize: 13668
[startup+70.0216 s]
Raw data (loadavg): 0.91 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3414 0 0 0 6980 10 0 0 25 0 1 0 548446009 15609856 3388 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3388 603 41 0 3770 0
vsize: 15244
[startup+80.022 s]
Raw data (loadavg): 0.93 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3415 0 0 0 7981 10 0 0 25 0 1 0 548446009 15609856 3389 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3389 603 41 0 3770 0
vsize: 15244
[startup+90.0312 s]
Raw data (loadavg): 0.94 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3415 0 0 0 8981 10 0 0 25 0 1 0 548446009 15609856 3389 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3389 603 41 0 3770 0
vsize: 15244
[startup+100.037 s]
Raw data (loadavg): 0.95 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3907 0 0 0 9980 12 0 0 25 0 1 0 548446009 17620992 3881 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4302 3881 603 41 0 4261 0
vsize: 17208
[startup+110.037 s]
Raw data (loadavg): 0.95 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3907 0 0 0 10980 12 0 0 25 0 1 0 548446009 17620992 3881 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4302 3881 603 41 0 4261 0
vsize: 17208
[startup+120.038 s]
Raw data (loadavg): 0.96 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3907 0 0 0 11980 12 0 0 25 0 1 0 548446009 17620992 3881 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4302 3881 603 41 0 4261 0
vsize: 17208
[startup+130.037 s]
Raw data (loadavg): 0.97 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3907 0 0 0 12979 13 0 0 25 0 1 0 548446009 17620992 3881 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4302 3881 603 41 0 4261 0
vsize: 17208
[startup+140.038 s]
Raw data (loadavg): 0.97 0.95 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 3907 0 0 0 13979 13 0 0 25 0 1 0 548446009 17620992 3881 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4302 3881 603 41 0 4261 0
vsize: 17208
[startup+150.039 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 4234 0 0 0 14978 14 0 0 25 0 1 0 548446009 18964480 4208 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4630 4208 603 41 0 4589 0
vsize: 18520
[startup+160.039 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 4575 0 0 0 15977 15 0 0 25 0 1 0 548446009 20443136 4549 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4991 4549 603 41 0 4950 0
vsize: 19964
[startup+170.039 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 4900 0 0 0 16975 17 0 0 25 0 1 0 548446009 21790720 4874 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5320 4874 603 41 0 5279 0
vsize: 21280
[startup+180.047 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5268 0 0 0 17975 18 0 0 25 0 1 0 548446009 23277568 5242 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5683 5242 603 41 0 5642 0
vsize: 22732
[startup+190.06 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5699 0 0 0 18974 20 0 0 25 0 1 0 548446009 25022464 5673 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6109 5673 603 41 0 6068 0
vsize: 24436
[startup+200.061 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5822 0 0 0 19973 22 0 0 25 0 1 0 548446009 25559040 5796 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6240 5796 603 41 0 6199 0
vsize: 24960
[startup+210.061 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5822 0 0 0 20973 22 0 0 25 0 1 0 548446009 25559040 5796 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6240 5796 603 41 0 6199 0
vsize: 24960
[startup+220.082 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5822 0 0 0 21974 22 0 0 25 0 1 0 548446009 25559040 5796 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6240 5796 603 41 0 6199 0
vsize: 24960
[startup+230.083 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5822 0 0 0 22974 23 0 0 25 0 1 0 548446009 25559040 5796 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6240 5796 603 41 0 6199 0
vsize: 24960
[startup+240.097 s]
Raw data (loadavg): 0.99 0.96 0.94 3/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5822 0 0 0 23975 23 0 0 25 0 1 0 548446009 25559040 5796 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6240 5796 603 41 0 6199 0
vsize: 24960
[startup+250.097 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5822 0 0 0 24976 23 0 0 25 0 1 0 548446009 25559040 5796 4294967295 134512640 134672761 3221224528 3221223632 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6240 5796 603 41 0 6199 0
vsize: 24960
[startup+260.098 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 5822 0 0 0 25976 23 0 0 25 0 1 0 548446009 25559040 5796 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6240 5796 603 41 0 6199 0
vsize: 24960
[startup+270.099 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 6109 0 0 0 26975 24 0 0 25 0 1 0 548446009 26755072 6083 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6532 6083 603 41 0 6491 0
vsize: 26128
[startup+280.106 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 6550 0 0 0 27975 25 0 0 25 0 1 0 548446009 28491776 6524 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6956 6524 603 41 0 6915 0
vsize: 27824
[startup+290.118 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 6969 0 0 0 28975 26 0 0 25 0 1 0 548446009 30240768 6943 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7383 6943 603 41 0 7342 0
vsize: 29532
[startup+300.137 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7209 0 0 0 29976 27 0 0 25 0 1 0 548446009 31182848 7183 4294967295 134512640 134672761 3221224528 3221223696 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 7183 603 41 0 7572 0
vsize: 30452
[startup+310.136 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7209 0 0 0 30976 27 0 0 25 0 1 0 548446009 31182848 7183 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 7183 603 41 0 7572 0
vsize: 30452
[startup+320.137 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7209 0 0 0 31977 27 0 0 25 0 1 0 548446009 31182848 7183 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 7183 603 41 0 7572 0
vsize: 30452
[startup+330.137 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7209 0 0 0 32977 27 0 0 25 0 1 0 548446009 31182848 7183 4294967295 134512640 134672761 3221224528 3221223728 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 7183 603 41 0 7572 0
vsize: 30452
[startup+340.138 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7209 0 0 0 33977 27 0 0 25 0 1 0 548446009 31182848 7183 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 7183 603 41 0 7572 0
vsize: 30452
[startup+350.138 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7209 0 0 0 34977 27 0 0 25 0 1 0 548446009 31182848 7183 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 7183 603 41 0 7572 0
vsize: 30452
[startup+360.145 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7209 0 0 0 35978 27 0 0 25 0 1 0 548446009 31182848 7183 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 7183 603 41 0 7572 0
vsize: 30452
[startup+370.151 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7322 0 0 0 36978 28 0 0 25 0 1 0 548446009 31723520 7296 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7745 7296 603 41 0 7704 0
vsize: 30980
[startup+380.151 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 7709 0 0 0 37978 28 0 0 25 0 1 0 548446009 33206272 7683 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8107 7683 603 41 0 8066 0
vsize: 32428
[startup+390.161 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8033 0 0 0 38978 30 0 0 25 0 1 0 548446009 34545664 8007 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8434 8007 603 41 0 8393 0
vsize: 33736
[startup+400.168 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 39976 31 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+410.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 40976 31 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+420.176 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 41977 31 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+430.181 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 42977 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+440.191 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 43978 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223632 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+450.19 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 44978 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+460.19 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 45977 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+470.198 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 46978 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+480.197 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 47978 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+490.206 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 48979 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+500.212 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 49979 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+510.211 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 50979 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223632 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+520.211 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 51979 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+530.217 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 52980 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+540.217 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 53980 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+550.217 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 54980 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+560.217 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 55980 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+570.217 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 56981 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+580.225 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 57981 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+590.228 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 58982 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+600.231 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 59982 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+610.231 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 60982 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+620.232 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27013
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 61983 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+630.231 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 27066
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 62982 32 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+640.233 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 27066
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 63982 33 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+650.232 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 27066
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 64982 33 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+660.232 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 27066
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 65982 33 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+670.233 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 27066
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 66982 33 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223712 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+680.232 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 27066
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 67982 34 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+690.232 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 27066
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 68981 34 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+700.233 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 27066
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 69981 35 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+710.234 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 70981 35 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+720.234 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 71981 35 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+730.234 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 72981 36 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+740.235 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 73981 36 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+750.234 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 74981 36 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+760.235 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 75981 36 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+770.235 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 76981 36 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+780.236 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8232 0 0 0 77981 36 0 0 25 0 1 0 548446009 35348480 8206 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8630 8206 603 41 0 8589 0
vsize: 34520
[startup+790.236 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8233 0 0 0 78981 36 0 0 25 0 1 0 548446009 35348480 8207 4294967295 134512640 134672761 3221224528 3221223712 134559176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8207 603 41 0 8589 0
vsize: 34520
[startup+800.236 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8233 0 0 0 79981 36 0 0 25 0 1 0 548446009 35348480 8207 4294967295 134512640 134672761 3221224528 3221223528 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8207 603 41 0 8589 0
vsize: 34520
[startup+810.236 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8233 0 0 0 80981 36 0 0 25 0 1 0 548446009 35348480 8207 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8207 603 41 0 8589 0
vsize: 34520
[startup+820.236 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8233 0 0 0 81981 37 0 0 25 0 1 0 548446009 35348480 8207 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8207 603 41 0 8589 0
vsize: 34520
[startup+830.243 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8233 0 0 0 82982 37 0 0 25 0 1 0 548446009 35348480 8207 4294967295 134512640 134672761 3221224528 3221223544 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8207 603 41 0 8589 0
vsize: 34520
[startup+840.243 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8233 0 0 0 83982 37 0 0 25 0 1 0 548446009 35348480 8207 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8207 603 41 0 8589 0
vsize: 34520
[startup+850.243 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8233 0 0 0 84982 37 0 0 25 0 1 0 548446009 35348480 8207 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8207 603 41 0 8589 0
vsize: 34520
[startup+860.242 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8233 0 0 0 85983 37 0 0 25 0 1 0 548446009 35348480 8207 4294967295 134512640 134672761 3221224528 3221223632 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8207 603 41 0 8589 0
vsize: 34520
[startup+870.242 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 86983 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+880.246 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 87983 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+890.247 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 88984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+900.247 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 89984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+910.247 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 90984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223712 134559173 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+920.247 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 91983 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+930.247 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 92984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+940.247 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 93984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+950.248 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 94984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+960.248 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27068
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 95984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+970.248 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 96984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+980.248 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 97984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+990.249 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 98984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1000.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 99984 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1010.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 100985 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223716 1075347078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1020.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 101985 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1030.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 102985 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1040.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 103985 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1050.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 104985 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1060.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 105985 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223664 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1070.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 106986 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1080.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 107986 37 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1090.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 108986 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223712 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1100.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 109986 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1110.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 110986 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1120.25 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 111986 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1130.26 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 112987 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1140.26 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 113987 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223632 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1150.26 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 114987 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1160.26 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 115987 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1170.26 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 116987 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1180.26 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 117987 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1190.26 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 118988 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
[startup+1200.26 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27070
Raw data (stat): 27013 (minisat+) R 27012 18865 18864 0 -1 0 8234 0 0 0 119988 38 0 0 25 0 1 0 548446009 35348480 8208 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 8208 603 41 0 8589 0
vsize: 34520
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.28 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 27070
Raw data (stat): 27013 (minisat+) Z 27012 18865 18864 0 -1 12 8237 0 0 0 119988 39 0 0 25 0 1 0 548446009 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.28
CPU time (s): 1200.28
CPU user time (s): 1199.88
CPU system time (s): 0.399939
CPU usage (%): 100.001
Max. virtual memory (Kb): 34520
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####