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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:98.opb
MD5SUM	ac510382bae6003fe0373ad32fd0064f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5
Optimality of the best value was proved	NO
Number of terms in the objective function	411
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	1129
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	1129
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03584
Number of variables	411
Total number of constraints	887
Number of constraints which are clauses	387
Number of constraints which are cardinality constraints (but not clauses)	500
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	16
Trace number 5097

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-13 21:55:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3308 boxname=wulflinc3 idbench=368 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ac510382bae6003fe0373ad32fd0064f  /oldhome/oroussel/tmp/wulflinc3/normalized-10:10:4.5:0.95:98.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc3/normalized-10:10:4.5:0.95:98.opb
IDLAUNCH: 3308
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 2
cpu MHz		: 451.190
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:        911044 kB
Buffers:         35228 kB
Cached:          65604 kB
SwapCached:       3276 kB
Active:          67896 kB
Inactive:        39060 kB
HighTotal:      131008 kB
HighFree:        61460 kB
LowTotal:       903652 kB
LowFree:        849584 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11092 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:15:41 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 3308 7 1200.32 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 476 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:    5
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   17
c ---[  81]---> BDD-cost:   21
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   17
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   17
c ---[  74]---> BDD-cost:   23
c ---[  73]---> BDD-cost:   26
c ---[  72]---> BDD-cost:   26
c ---[  71]---> BDD-cost:   32
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   23
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   29
c ---[  61]---> BDD-cost:   32
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   23
c ---[  58]---> BDD-cost:   23
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   26
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   41
c ---[  50]---> BDD-cost:   38
c ---[  49]---> BDD-cost:   26
c ---[  48]---> BDD-cost:   24
c ---[  47]---> BDD-cost:   20
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   32
c ---[  41]---> BDD-cost:   38
c ---[  40]---> BDD-cost:   32
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   23
c ---[  36]---> BDD-cost:    7
c ---[  35]---> BDD-cost:   20
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   32
c ---[  30]---> BDD-cost:   29
c ---[  29]---> BDD-cost:   23
c ---[  28]---> BDD-cost:   23
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   23
c ---[  22]---> BDD-cost:   29
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   23
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   17
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   23
c ---[  12]---> BDD-cost:   20
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   11
c ---[   9]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    7
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4472    12709 |    1490       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 398[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23127     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   32494    78480 |   10831       0        0     nan |  0.000 % |
c |       102 |   32227    77921 |   11914      93     1757    18.9 |  1.135 % |
c ==============================================================================
c [1mFound solution: 43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       161 |   44201   105933 |   14733     151     2760    18.3 |  1.135 % |
c |       261 |   44201   105933 |   16206     251     7069    28.2 |  1.191 % |
c |       411 |   44129   105785 |   17826     368     8799    23.9 |  1.364 % |
c |       636 |   43979   105462 |   19609     564    10452    18.5 |  1.761 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       858 |   44008   105544 |   14669     786    14574    18.5 |  1.761 % |
c |       958 |   44008   105544 |   16135     886    15808    17.8 |  1.764 % |
c |      1108 |   44008   105544 |   17749    1036    18772    18.1 |  1.764 % |
c |      1335 |   44008   105544 |   19524    1263    42756    33.9 |  1.764 % |
c |      1673 |   43872   105242 |   21476    1589    47389    29.8 |  2.038 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2115 |   43823   105162 |   14607    2030    58752    28.9 |  2.038 % |
c |      2215 |   43719   104928 |   16067    2128    61709    29.0 |  2.444 % |
c |      2367 |   43671   104819 |   17674    2277    64221    28.2 |  2.503 % |
c |      2592 |   43369   104134 |   19441    2494    73322    29.4 |  3.036 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2850 |   43376   104156 |   14458    2752    80617    29.3 |  3.036 % |
c |      2950 |   43376   104156 |   15903    2852    81890    28.7 |  3.040 % |
c |      3100 |   43376   104156 |   17494    3002    83094    27.7 |  3.040 % |
c |      3326 |   43376   104156 |   19243    3228    90300    28.0 |  3.040 % |
c |      3663 |   43209   103775 |   21167    3563   100193    28.1 |  3.345 % |
c |      4172 |   43209   103775 |   23284    4072   113402    27.8 |  3.345 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4914 |   43272   103952 |   14424    4811   136307    28.3 |  3.345 % |
c |      5014 |   43177   103737 |   15866    4900   137820    28.1 |  3.483 % |
c |      5165 |   43177   103737 |   17453    5051   138864    27.5 |  3.483 % |
c |      5390 |   43177   103737 |   19198    5276   140350    26.6 |  3.483 % |
c |      5729 |   43177   103737 |   21118    5615   145264    25.9 |  3.483 % |
c |      6236 |   43165   103710 |   23229    6121   154621    25.3 |  3.497 % |
c |      6995 |   43072   103495 |   25552    6876   178998    26.0 |  3.710 % |
c |      8134 |   42972   103274 |   28108    8011   265475    33.1 |  3.914 % |
c |      9842 |   42943   103209 |   30919    9717   307744    31.7 |  3.996 % |
c |     12405 |   42943   103209 |   34011   12280   461530    37.6 |  3.996 % |
c |     16249 |   42943   103209 |   37412   16124   703042    43.6 |  3.996 % |
c |     22015 |   42912   103140 |   41153   21884  1438161    65.7 |  4.082 % |
c |     30666 |   42912   103140 |   45268   30535  2435749    79.8 |  4.082 % |
c |     43640 |   42912   103140 |   49795   43509  4226758    97.1 |  4.082 % |
c |     63102 |   42912   103140 |   54775   17575  3032611   172.6 |  4.082 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90954 |   42912   103147 |   14304   45424  8232293   181.2 |  4.082 % |
c |     91054 |   42912   103147 |   15734   14509  2806830   193.5 |  4.091 % |
c |     91204 |   42912   103147 |   17307   14659  2808371   191.6 |  4.091 % |
c |     91429 |   42912   103147 |   19038   14884  2812415   189.0 |  4.091 % |
c |     91770 |   42912   103147 |   20942   15225  2829835   185.9 |  4.091 % |
c |     92281 |   42894   103105 |   23036   15733  2837111   180.3 |  4.118 % |
c |     93040 |   42894   103105 |   25340   16492  2881603   174.7 |  4.118 % |
c |     94182 |   42894   103105 |   27874   17634  2927916   166.0 |  4.118 % |
c |     95892 |   42894   103105 |   30661   19344  3204381   165.7 |  4.118 % |
c |     98455 |   42894   103105 |   33728   21907  3314140   151.3 |  4.118 % |
c |    102302 |   42878   103068 |   37100   25751  3516726   136.6 |  4.141 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    105316 |   42860   103033 |   14286   28730  3799486   132.2 |  4.141 % |
c |    105419 |   42860   103033 |   15714   13143   878856    66.9 |  4.208 % |
c |    105569 |   42725   102721 |   17286   13287   879762    66.2 |  4.472 % |
c |    105794 |   42725   102721 |   19014   13512   882017    65.3 |  4.472 % |
c |    106131 |   42725   102721 |   20916   13849   890028    64.3 |  4.472 % |
c |    106637 |   42725   102721 |   23007   14355   901438    62.8 |  4.472 % |
c |    107397 |   42725   102721 |   25308   15115   934652    61.8 |  4.472 % |
c |    108537 |   42725   102721 |   27839   16255   992155    61.0 |  4.472 % |
c |    110245 |   42725   102721 |   30623   17963  1066105    59.4 |  4.472 % |
c |    112807 |   42725   102721 |   33685   20525  1332557    64.9 |  4.472 % |
c ==============================================================================
c [1mFound solution: 14[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114488 |   42751   102796 |   14250   22206  1371666    61.8 |  4.472 % |
c |    114588 |   42751   102796 |   15675   11203   491922    43.9 |  4.473 % |
c |    114738 |   42751   102796 |   17242   11353   494101    43.5 |  4.473 % |
c |    114963 |   42751   102796 |   18966   11578   503314    43.5 |  4.473 % |
c |    115302 |   42751   102796 |   20863   11917   516562    43.3 |  4.473 % |
c |    115808 |   42751   102796 |   22949   12423   563916    45.4 |  4.473 % |
c |    116567 |   42655   102580 |   25244   13181   579913    44.0 |  4.672 % |
c |    117706 |   42655   102580 |   27769   14320   642355    44.9 |  4.672 % |
c |    119414 |   42655   102580 |   30546   16028   754371    47.1 |  4.672 % |
c |    121977 |   42655   102580 |   33600   18591  1012810    54.5 |  4.672 % |
c ==============================================================================
c [1mFound solution: 11[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125422 |   42654   102599 |   14218   22024  1133680    51.5 |  4.672 % |
c |    125522 |   42654   102599 |   15639   11112   496118    44.6 |  4.750 % |
c |    125673 |   42654   102599 |   17203   11263   499510    44.3 |  4.750 % |
c |    125899 |   42654   102599 |   18924   11489   514157    44.8 |  4.750 % |
c |    126240 |   42650   102591 |   20816   11827   525001    44.4 |  4.754 % |
c |    126748 |   42650   102591 |   22898   12335   554839    45.0 |  4.754 % |
c |    127508 |   42650   102591 |   25188   13095   613587    46.9 |  4.754 % |
c |    128647 |   42650   102591 |   27706   14234   686549    48.2 |  4.754 % |
c |    130355 |   42650   102591 |   30477   15942   847139    53.1 |  4.754 % |
c |    132917 |   42650   102591 |   33525   18504   975950    52.7 |  4.754 % |
c |    136761 |   42650   102591 |   36877   22348  1557897    69.7 |  4.754 % |
c |    142528 |   42650   102591 |   40565   28115  2081293    74.0 |  4.754 % |
c |    151177 |   42650   102591 |   44622   36764  3716668   101.1 |  4.754 % |
c |    164151 |   42650   102591 |   49084   17638  1034620    58.7 |  4.754 % |
c |    183612 |   42650   102591 |   53992   37099  4369752   117.8 |  4.754 % |
c |    212804 |   42650   102591 |   59392   19896  2166225   108.9 |  4.754 % |
c |    256593 |   42650   102591 |   65331   63685 14315644   224.8 |  4.754 % |
c ==============================================================================
c [1mFound solution: 9[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    315536 |   42653   102605 |   14217   64339  9301830   144.6 |  4.754 % |
c |    315637 |   42653   102605 |   15638    8667   872064   100.6 |  4.762 % |
c |    315787 |   42653   102605 |   17202    8817   879176    99.7 |  4.762 % |
c |    316013 |   42653   102605 |   18922    9043   885390    97.9 |  4.762 % |
c |    316351 |   42653   102605 |   20815    9381   902282    96.2 |  4.762 % |
c |    316857 |   42653   102605 |   22896    9887   943964    95.5 |  4.762 % |
c |    317616 |   42641   102579 |   25186   10641   966354    90.8 |  4.794 % |
c |    318755 |   42641   102579 |   27704   11780  1004746    85.3 |  4.794 % |
c |    320465 |   42641   102579 |   30475   13490  1235075    91.6 |  4.794 % |
c |    323030 |   42641   102579 |   33522   16055  1348999    84.0 |  4.794 % |
c |    326875 |   42641   102579 |   36875   19900  1552401    78.0 |  4.794 % |
c |    332641 |   42641   102579 |   40562   25666  2398897    93.5 |  4.794 % |
#### 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.84 0.94 0.90 2/54 16432
Raw data (stat): 16432 (runsolver) R 16431 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421130210 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 2330 0 0 0 993 5 0 0 25 0 1 0 421130210 11538432 2254 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2817 2254 603 41 0 2776 0
vsize: 11268
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 2678 0 0 0 1991 6 0 0 25 0 1 0 421130210 13053952 2602 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3187 2602 603 41 0 3146 0
vsize: 12748
[startup+30.001 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 3048 0 0 0 2990 7 0 0 25 0 1 0 421130210 14536704 2972 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 2972 603 41 0 3508 0
vsize: 14196
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 3577 0 0 0 3988 10 0 0 25 0 1 0 421130210 16687104 3501 4294967295 134512640 134672761 3221224624 3221223808 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4074 3501 603 41 0 4033 0
vsize: 16296
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 4011 0 0 0 4987 11 0 0 25 0 1 0 421130210 18563072 3935 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4532 3935 603 41 0 4491 0
vsize: 18128
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 4437 0 0 0 5986 12 0 0 25 0 1 0 421130210 20295680 4361 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4955 4361 603 41 0 4914 0
vsize: 19820
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 4824 0 0 0 6985 13 0 0 25 0 1 0 421130210 21757952 4748 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5312 4748 603 41 0 5271 0
vsize: 21248
[startup+80.0045 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 5223 0 0 0 7984 15 0 0 25 0 1 0 421130210 23625728 5147 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5768 5147 603 41 0 5727 0
vsize: 23072
[startup+90.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 5631 0 0 0 8982 17 0 0 25 0 1 0 421130210 25255936 5555 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6166 5555 603 41 0 6125 0
vsize: 24664
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 5959 0 0 0 9981 17 0 0 25 0 1 0 421130210 26583040 5883 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5883 603 41 0 6449 0
vsize: 25960
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 6348 0 0 0 10981 18 0 0 25 0 1 0 421130210 28184576 6272 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6881 6273 603 41 0 6840 0
vsize: 27524
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 6737 0 0 0 11980 20 0 0 25 0 1 0 421130210 29782016 6661 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7271 6661 603 41 0 7230 0
vsize: 29084
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 7258 0 0 0 12978 22 0 0 25 0 1 0 421130210 31928320 7182 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7795 7182 603 41 0 7754 0
vsize: 31180
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 7783 0 0 0 13976 24 0 0 25 0 1 0 421130210 34058240 7707 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8315 7707 603 41 0 8274 0
vsize: 33260
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 8255 0 0 0 14976 25 0 0 25 0 1 0 421130210 35921920 8179 4294967295 134512640 134672761 3221224624 3221223728 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8770 8179 603 41 0 8729 0
vsize: 35080
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 8703 0 0 0 15974 27 0 0 25 0 1 0 421130210 37793792 8627 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9227 8627 603 41 0 9186 0
vsize: 36908
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 9158 0 0 0 16973 28 0 0 25 0 1 0 421130210 39669760 9082 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9685 9082 603 41 0 9644 0
vsize: 38740
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 9596 0 0 0 17971 30 0 0 25 0 1 0 421130210 41402368 9520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10108 9520 603 41 0 10067 0
vsize: 40432
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 18970 31 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+200.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 19970 31 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 20969 31 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223824 134557796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 21969 31 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 22970 31 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 23969 31 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 24969 32 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16432
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 25969 32 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223808 134558859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+270.011 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 16485
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 26969 32 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+280.011 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 16485
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 27968 32 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+290.013 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 16485
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10015 0 0 0 28969 32 0 0 25 0 1 0 421130210 43147264 9939 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9939 603 41 0 10493 0
vsize: 42136
[startup+300.013 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 16485
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10231 0 0 0 29968 33 0 0 25 0 1 0 421130210 43954176 10155 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10731 10155 603 41 0 10690 0
vsize: 42924
[startup+310.013 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 16485
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10702 0 0 0 30967 34 0 0 25 0 1 0 421130210 45953024 10626 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11219 10626 603 41 0 11178 0
vsize: 44876
[startup+320.014 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 16485
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 31965 36 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+330.013 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 16485
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 32965 36 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+340.014 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 33965 37 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+350.013 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 34964 37 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+360.013 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 35964 37 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+370.014 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 36964 37 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+380.014 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 37964 38 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+390.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 38964 38 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+400.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 39964 38 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+410.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 40963 39 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+420.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 41964 39 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+430.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 42963 39 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+440.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 43964 39 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+450.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 44964 39 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+460.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 45964 40 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223776 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+470.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 46964 40 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223824 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+480.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10975 0 0 0 47964 40 0 0 25 0 1 0 421130210 47034368 10899 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10899 603 41 0 11442 0
vsize: 45932
[startup+490.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 48964 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+500.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 49965 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+510.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 50965 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+520.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 51965 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+530.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 52965 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+540.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 53965 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+550.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 54966 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+560.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 55966 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+570.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16487
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 56966 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+580.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 57966 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+590.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 58966 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+600.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 59966 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+610.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 60967 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+620.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10976 0 0 0 61967 40 0 0 25 0 1 0 421130210 47034368 10900 4294967295 134512640 134672761 3221224624 3221223728 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10900 603 41 0 11442 0
vsize: 45932
[startup+630.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 62967 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+640.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 63967 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+650.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 64967 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+660.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 65967 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+670.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 66968 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+680.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 67968 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+690.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 68968 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+700.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 69968 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223768 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+710.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 70968 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+720.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 71969 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+730.027 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 72969 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+740.028 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 73969 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+750.028 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 10978 0 0 0 74969 40 0 0 25 0 1 0 421130210 47034368 10902 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11483 10902 603 41 0 11442 0
vsize: 45932
[startup+760.028 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 11410 0 0 0 75968 41 0 0 25 0 1 0 421130210 48758784 11334 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11904 11334 603 41 0 11863 0
vsize: 47616
[startup+770.029 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 11893 0 0 0 76967 42 0 0 25 0 1 0 421130210 50774016 11817 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12396 11817 603 41 0 12355 0
vsize: 49584
[startup+780.029 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 12318 0 0 0 77966 43 0 0 25 0 1 0 421130210 52531200 12242 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12825 12242 603 41 0 12784 0
vsize: 51300
[startup+790.029 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 12727 0 0 0 78965 45 0 0 25 0 1 0 421130210 54132736 12651 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13216 12651 603 41 0 13175 0
vsize: 52864
[startup+800.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 13098 0 0 0 79964 45 0 0 25 0 1 0 421130210 55721984 13022 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13604 13022 603 41 0 13563 0
vsize: 54416
[startup+810.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 13488 0 0 0 80964 46 0 0 25 0 1 0 421130210 57335808 13412 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13998 13412 603 41 0 13957 0
vsize: 55992
[startup+820.031 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 13961 0 0 0 81963 48 0 0 25 0 1 0 421130210 59215872 13885 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14457 13885 603 41 0 14416 0
vsize: 57828
[startup+830.032 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 14351 0 0 0 82961 49 0 0 25 0 1 0 421130210 60821504 14275 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14849 14275 603 41 0 14808 0
vsize: 59396
[startup+840.033 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 14773 0 0 0 83961 50 0 0 25 0 1 0 421130210 62562304 14697 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15274 14697 603 41 0 15233 0
vsize: 61096
[startup+850.033 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 15210 0 0 0 84959 52 0 0 25 0 1 0 421130210 64425984 15134 4294967295 134512640 134672761 3221224624 3221223728 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15729 15134 603 41 0 15688 0
vsize: 62916
[startup+860.032 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 15629 0 0 0 85959 53 0 0 25 0 1 0 421130210 66039808 15553 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16123 15553 603 41 0 16082 0
vsize: 64492
[startup+870.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 16048 0 0 0 86958 53 0 0 25 0 1 0 421130210 67776512 15972 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16547 15972 603 41 0 16506 0
vsize: 66188
[startup+880.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 16457 0 0 0 87957 54 0 0 25 0 1 0 421130210 69521408 16381 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16973 16381 603 41 0 16932 0
vsize: 67892
[startup+890.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 16791 0 0 0 88957 55 0 0 25 0 1 0 421130210 70852608 16715 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17298 16715 603 41 0 17257 0
vsize: 69192
[startup+900.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 17183 0 0 0 89956 55 0 0 25 0 1 0 421130210 72450048 17107 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17688 17107 603 41 0 17647 0
vsize: 70752
[startup+910.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 17538 0 0 0 90956 56 0 0 25 0 1 0 421130210 73912320 17462 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18045 17462 603 41 0 18004 0
vsize: 72180
[startup+920.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 17877 0 0 0 91955 57 0 0 25 0 1 0 421130210 75390976 17801 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18406 17801 603 41 0 18365 0
vsize: 73624
[startup+930.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 18326 0 0 0 92953 59 0 0 25 0 1 0 421130210 77398016 18250 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18896 18250 603 41 0 18855 0
vsize: 75584
[startup+940.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 18777 0 0 0 93952 60 0 0 25 0 1 0 421130210 79265792 18701 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19352 18701 603 41 0 19311 0
vsize: 77408
[startup+950.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 19253 0 0 0 94951 61 0 0 25 0 1 0 421130210 81260544 19177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19839 19177 603 41 0 19798 0
vsize: 79356
[startup+960.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 19709 0 0 0 95949 63 0 0 25 0 1 0 421130210 83132416 19633 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20296 19633 603 41 0 20255 0
vsize: 81184
[startup+970.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20140 0 0 0 96948 65 0 0 25 0 1 0 421130210 84877312 20064 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20722 20064 603 41 0 20681 0
vsize: 82888
[startup+980.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 97947 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+990.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 98948 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 99948 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 100948 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 101948 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 102948 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 103948 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 104949 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 105949 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223728 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 106949 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 107949 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223808 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 108950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 109950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223808 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 110950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 111950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 112950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 113950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 114951 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 115950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 116950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 117950 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1190.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 118961 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16489
Raw data (stat): 16432 (minisat+) R 16431 10720 10719 0 -1 0 20309 0 0 0 119961 66 0 0 25 0 1 0 421130210 85544960 20233 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20233 603 41 0 20844 0
vsize: 83540
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 16489
Raw data (stat): 16432 (minisat+) Z 16431 10720 10719 0 -1 12 20312 0 0 0 119961 70 0 0 25 0 1 0 421130210 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.19
CPU time (s): 1200.32
CPU user time (s): 1199.62
CPU system time (s): 0.700893
CPU usage (%): 100.011
Max. virtual memory (Kb): 83540
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####