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-gt2.opb
MD5SUM	f1382105ee9fb79777762a53cf6a73c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	21166
Optimality of the best value was proved	NO
Number of terms in the objective function	304
Biggest coefficient in the objective function	62376
Number of bits for the biggest coefficient in the objective function	16
Sum of the numbers in the objective function	3092598
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	62376
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	3092598
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.14
Number of variables	556
Total number of constraints	217
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	191
Minimum length of a constraint	1
Maximum length of a constraint	48
Trace number 31210

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-05-25 23:03:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22603 boxname=wulflinc22 idbench=1419 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  f1382105ee9fb79777762a53cf6a73c1  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-gt2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-gt2.opb
IDLAUNCH: 22603
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        592712 kB
Buffers:         35620 kB
Cached:         383948 kB
SwapCached:        400 kB
Active:          62832 kB
Inactive:       359016 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        592460 kB
SwapTotal:     2097892 kB
SwapFree:      2096804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5580 kB
Slab:            14260 kB
Committed_AS:    63572 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 23:23:34 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 22603 7 1229.9 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................ssssssssss
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  71]---> BDD-cost:    2
c ---[  70]---> BDD-cost:    2
c ---[  68]---> BDD-cost:    2
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  37]---> BDD-cost:  107
c ---[  36]---> Sorter-cost:  778     Base: 2 2 2
c ---[  35]---> Sorter-cost:  777     Base: 2 2 2
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:  183
c ---[  31]---> BDD-cost:   25
c ---[  30]---> Sorter-cost:  379     Base: 2 2 2
c ---[  29]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  128
c ---[  27]---> BDD-cost:  105
c ---[  26]---> Sorter-cost:  778     Base: 2 2 2
c ---[  25]---> BDD-cost:  111
c ---[  24]---> BDD-cost:  105
c ---[  23]---> BDD-cost:   54
c ---[  22]---> BDD-cost:   54
c ---[  21]---> BDD-cost:   21
c ---[  15]---> Adder-cost: 273   maxlim: 12127   bits: 15/14
c ---[   9]---> Sorter-cost: 2085     Base: 2 5 2 2 2
c ---[   8]---> BDD-cost:   76
c ---[   7]---> Sorter-cost: 2550     Base: 2 5 2 2 2
c ---[   6]---> Adder-cost: 223   maxlim: 249   bits: 9/8
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:  114
c ---[   3]---> BDD-cost:   55
c ---[   2]---> Sorter-cost: 2935     Base: 2 5 2 2 2 2
c ---[   1]---> Adder-cost: 212   maxlim: 230   bits: 9/8
c ---[   0]---> BDD-cost:   92
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   30742    79537 |   10247       0        0     nan |  0.000 % |
c |       100 |   30742    79537 |   11271     100      544     5.4 |  0.987 % |
c |       250 |   30742    79537 |   12398     250     2459     9.8 |  0.986 % |
c |       477 |   30742    79537 |   13638     477     3973     8.3 |  0.986 % |
c ==============================================================================
c [1mFound solution: 175459[0m
c ---[   0]---> Sorter-cost:92424     Base: 2 2 2 3 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 |       637 |  284458   671673 |   94819     637    11349    17.8 |  0.986 % |
c |       737 |  284437   671627 |  104300     735    12835    17.5 |  0.117 % |
c |       887 |  284035   670723 |  114730     880    13845    15.7 |  0.221 % |
c |      1114 |  284035   670723 |  126204    1107    15250    13.8 |  0.221 % |
c |      1451 |  284035   670723 |  138824    1444    17597    12.2 |  0.221 % |
c |      1958 |  282828   667995 |  152706    1939    63559    32.8 |  0.549 % |
c |      2717 |  282661   667617 |  167977    2697   148878    55.2 |  0.596 % |
c |      3856 |  271841   642801 |  184775    3781   190178    50.3 |  3.911 % |
c |      5565 |  267485   632765 |  203252    5455   244772    44.9 |  5.294 % |
c |      8129 |  258374   611785 |  223578    7920   366516    46.3 |  8.175 % |
c |     11974 |  255958   606212 |  245936   11748   726453    61.8 |  8.939 % |
c |     17740 |  250695   594032 |  270529   17444  1194291    68.5 | 10.666 % |
c |     26390 |  249167   590517 |  297582   26068  1851301    71.0 | 11.165 % |
c |     39364 |  243608   577673 |  327340   38951  2440127    62.6 | 12.969 % |
c ==============================================================================
c [1mFound solution: 174126[0m
c ---[   0]---> Sorter-cost:70620     Base: 2 2 2 3 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 |     57904 |  404098   950841 |  134699   57401  4098734    71.4 | 12.969 % |
c |     58008 |  403639   949827 |  148168   57502  4100867    71.3 | 14.245 % |
c |     58159 |  402994   948375 |  162985   57644  4103732    71.2 | 14.375 % |
c |     58384 |  402994   948375 |  179284   57869  4109174    71.0 | 14.375 % |
c |     58721 |  401268   944466 |  197212   58185  4111678    70.7 | 14.715 % |
c |     59229 |  401268   944466 |  216934   58693  4136023    70.5 | 14.715 % |
c |     59988 |  401268   944466 |  238627   59452  4283010    72.0 | 14.715 % |
c |     61127 |  401110   944098 |  262490   60582  4296313    70.9 | 14.748 % |
c |     62836 |  400965   943764 |  288739   62290  4391753    70.5 | 14.776 % |
c |     65398 |  397076   934924 |  317613   64748  4501421    69.5 | 15.543 % |
c |     69242 |  396305   933196 |  349374   68585  4939320    72.0 | 15.693 % |
c ==============================================================================
c [1mFound solution: 172189[0m
c ---[   0]---> Sorter-cost:69141     Base: 2 2 2 3 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 |     73398 |  544035  1277084 |  181345   72562  5065701    69.8 | 15.693 % |
c |     73498 |  544035  1277084 |  199479   72662  5068684    69.8 | 16.507 % |
c |     73648 |  544035  1277084 |  219427   72812  5070213    69.6 | 16.507 % |
c |     73873 |  543068  1274852 |  241370   72952  5097260    69.9 | 16.641 % |
c |     74210 |  540987  1270145 |  265507   73257  5099628    69.6 | 16.928 % |
c |     74716 |  540190  1268331 |  292057   73706  5103053    69.2 | 17.043 % |
c |     75475 |  536077  1259024 |  321263   74187  5111911    68.9 | 17.612 % |
c |     76614 |  536077  1259024 |  353390   75326  5156748    68.5 | 17.612 % |
c |     78323 |  530933  1247267 |  388729   76556  5221852    68.2 | 18.328 % |
c ==============================================================================
c [1mFound solution: 165654[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 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 |     78741 |  531464  1248864 |  177154   76974  5254301    68.3 | 18.328 % |
c |     78842 |  530814  1247415 |  194869   77072  5256580    68.2 | 18.396 % |
c |     78994 |  530399  1246465 |  214356   77218  5264119    68.2 | 18.455 % |
c |     79219 |  530399  1246465 |  235791   77443  5280849    68.2 | 18.455 % |
c |     79556 |  530293  1246228 |  259371   77779  5290167    68.0 | 18.466 % |
c |     80062 |  530239  1246109 |  285308   78283  5319511    68.0 | 18.473 % |
c |     80821 |  530239  1246109 |  313839   79042  5399819    68.3 | 18.473 % |
c |     81960 |  530034  1245656 |  345223   80180  5665661    70.7 | 18.500 % |
c |     83669 |  524072  1232048 |  379745   81399  5764458    70.8 | 19.341 % |
c |     86231 |  522340  1228063 |  417719   83937  5900609    70.3 | 19.584 % |
c ==============================================================================
c [1mFound solution: 165192[0m
c ---[   0]---> Sorter-cost:68242     Base: 2 2 2 3 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 |     87232 |  675287  1583479 |  225095   84938  6115837    72.0 | 19.584 % |
c |     87332 |  675287  1583479 |  247604   85038  6117351    71.9 | 19.030 % |
c |     87483 |  673704  1579889 |  272364   85180  6121380    71.9 | 19.205 % |
c |     87709 |  673704  1579889 |  299601   85406  6147900    72.0 | 19.205 % |
c |     88046 |  673704  1579889 |  329561   85743  6190662    72.2 | 19.205 % |
c |     88553 |  673704  1579889 |  362517   86250  6204900    71.9 | 19.205 % |
c |     89314 |  673704  1579889 |  398769   87011  6265601    72.0 | 19.205 % |
c |     90456 |  668664  1568463 |  438646   88034  6376824    72.4 | 19.756 % |
c |     92164 |  666346  1563278 |  482511   89724  6660716    74.2 | 20.003 % |
c |     94726 |  666346  1563278 |  530762   92286  7009786    76.0 | 20.003 % |
c |     98570 |  664362  1558830 |  583838   96127  7652673    79.6 | 20.223 % |
c ==============================================================================
c [1mFound solution: 164617[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 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 |     98680 |  664408  1559385 |  221469   96237  7659605    79.6 | 20.223 % |
c |     98781 |  664408  1559385 |  243615   96338  7666260    79.6 | 20.222 % |
c |     98931 |  663882  1558213 |  267977   96478  7669094    79.5 | 20.280 % |
c |     99156 |  663882  1558213 |  294775   96703  7674639    79.4 | 20.280 % |
c |     99494 |  663882  1558213 |  324252   97041  7682075    79.2 | 20.280 % |
c |    100000 |  662711  1555549 |  356678   97537  7702428    79.0 | 20.411 % |
c |    100761 |  658022  1544826 |  392345   98090  7724938    78.8 | 20.924 % |
c |    101902 |  657896  1544545 |  431580   99228  7828742    78.9 | 20.939 % |
c |    103612 |  656006  1540264 |  474738  100809  7919978    78.6 | 21.151 % |
c |    106174 |  653447  1534433 |  522212  103311  8338281    80.7 | 21.441 % |
c |    110018 |  653447  1534433 |  574433  107155  8992194    83.9 | 21.441 % |
c |    115784 |  650518  1527749 |  631876  112772  9214928    81.7 | 21.761 % |
c |    124433 |  650518  1527749 |  695064  121421  9889029    81.4 | 21.761 % |
c ==============================================================================
c [1mFound solution: 163483[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 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 |    131430 |  646191  1517922 |  215397  128336 10361434    80.7 | 21.761 % |
c |    131530 |  646191  1517922 |  236936  128436 10366789    80.7 | 22.242 % |
c |    131680 |  646026  1517552 |  260630  128583 10382200    80.7 | 22.260 % |
c |    131906 |  646026  1517552 |  286693  128809 10384118    80.6 | 22.260 % |
c |    132243 |  646026  1517552 |  315362  129146 10387012    80.4 | 22.260 % |
c |    132750 |  645201  1515676 |  346899  129631 10391486    80.2 | 22.349 % |
c |    133510 |  642926  1510464 |  381588  130236 10419037    80.0 | 22.602 % |
c |    134650 |  642926  1510464 |  419747  131376 10465729    79.7 | 22.602 % |
c ==============================================================================
c [1mFound solution: 161824[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 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 |    135225 |  642822  1510228 |  214274  131950 10510329    79.7 | 22.602 % |
c |    135328 |  642822  1510228 |  235701  132053 10515914    79.6 | 22.614 % |
c |    135478 |  642047  1508455 |  259271  132190 10518344    79.6 | 22.694 % |
c |    135703 |  642047  1508455 |  285198  132415 10522658    79.5 | 22.694 % |
c |    136040 |  641491  1507180 |  313718  132743 10524190    79.3 | 22.755 % |
c |    136547 |  641393  1506955 |  345090  133249 10584627    79.4 | 22.766 % |
c |    137306 |  641201  1506523 |  379599  134000 10677526    79.7 | 22.785 % |
c |    138445 |  640805  1505618 |  417559  135124 10695361    79.2 | 22.828 % |
c |    140154 |  637215  1497411 |  459315  136401 10708038    78.5 | 23.224 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  8690 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.98 0.91 2/54 8686
Raw data (stat): 8686 (runsolver) R 8685 23310 23309 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842687847 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.0026 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.0027 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.0027 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.0034 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.0028 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.0038 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.0045 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.0039 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8690
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 3/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.74 s]
Raw data (loadavg): 0.99 0.98 0.91 1/53 8692
Raw data (stat): 8686 (minisat+_script) S 8685 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842687847 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.74
CPU time (s): 1229.9
CPU user time (s): 1228.9
CPU system time (s): 1.00385
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####