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 6047

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 03:14:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4504 boxname=wulflinc21 idbench=368 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ac510382bae6003fe0373ad32fd0064f  /oldhome/oroussel/tmp/wulflinc21/normalized-10:10:4.5:0.95:98.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc21/normalized-10:10:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc21/normalized-10:10:4.5:0.95:98.opb
IDLAUNCH: 4504
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        876208 kB
Buffers:         28324 kB
Cached:         110260 kB
SwapCached:          0 kB
Active:          37016 kB
Inactive:       104412 kB
HighTotal:      131008 kB
HighFree:        17108 kB
LowTotal:       903652 kB
LowFree:        859100 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              56 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11396 kB
Committed_AS:    63824 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:34:07 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4504 7 1200.2 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.92 0.97 0.91 2/55 3873
Raw data (stat): 3873 (runsolver) R 3872 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 358529568 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99954 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 2313 0 0 0 994 4 0 0 25 0 1 0 358529568 11472896 2235 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2801 2235 603 41 0 2760 0
vsize: 11204
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 2667 0 0 0 1993 6 0 0 25 0 1 0 358529568 13000704 2589 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3174 2589 603 41 0 3133 0
vsize: 12696
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 3043 0 0 0 2992 7 0 0 25 0 1 0 358529568 14610432 2965 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3567 2965 603 41 0 3526 0
vsize: 14268
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 3581 0 0 0 3989 9 0 0 25 0 1 0 358529568 16748544 3503 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3503 603 41 0 4048 0
vsize: 16356
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 4018 0 0 0 4988 11 0 0 25 0 1 0 358529568 18489344 3940 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4514 3940 603 41 0 4473 0
vsize: 18056
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 4445 0 0 0 5987 12 0 0 25 0 1 0 358529568 20230144 4367 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4939 4367 603 41 0 4898 0
vsize: 19756
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 4825 0 0 0 6986 13 0 0 25 0 1 0 358529568 21839872 4747 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5332 4747 603 41 0 5291 0
vsize: 21328
[startup+80.0033 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 5236 0 0 0 7985 14 0 0 25 0 1 0 358529568 23572480 5158 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5755 5158 603 41 0 5714 0
vsize: 23020
[startup+90.0039 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 5653 0 0 0 8984 15 0 0 25 0 1 0 358529568 25329664 5575 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6184 5575 603 41 0 6143 0
vsize: 24736
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 5981 0 0 0 9983 17 0 0 25 0 1 0 358529568 26652672 5903 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6507 5903 603 41 0 6466 0
vsize: 26028
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 6374 0 0 0 10982 18 0 0 25 0 1 0 358529568 28241920 6296 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6895 6296 603 41 0 6854 0
vsize: 27580
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 6776 0 0 0 11981 19 0 0 25 0 1 0 358529568 29974528 6698 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7318 6698 603 41 0 7277 0
vsize: 29272
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 7314 0 0 0 12980 20 0 0 25 0 1 0 358529568 32116736 7236 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7841 7236 603 41 0 7800 0
vsize: 31364
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 7832 0 0 0 13979 21 0 0 25 0 1 0 358529568 34263040 7754 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8365 7754 603 41 0 8324 0
vsize: 33460
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 8318 0 0 0 14977 23 0 0 25 0 1 0 358529568 36134912 8240 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8822 8240 603 41 0 8781 0
vsize: 35288
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 8768 0 0 0 15977 24 0 0 25 0 1 0 358529568 37994496 8690 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9276 8690 603 41 0 9235 0
vsize: 37104
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9223 0 0 0 16975 25 0 0 25 0 1 0 358529568 39866368 9145 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9733 9145 603 41 0 9692 0
vsize: 38932
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9686 0 0 0 17974 26 0 0 25 0 1 0 358529568 41742336 9608 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10191 9608 603 41 0 10150 0
vsize: 40764
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 18973 28 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 19973 28 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 20973 28 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 21973 28 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 22973 28 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 23973 28 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 24973 28 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 25973 29 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 26973 29 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 27973 29 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 9997 0 0 0 28973 29 0 0 25 0 1 0 358529568 43085824 9919 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10519 9919 603 41 0 10478 0
vsize: 42076
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10347 0 0 0 29972 30 0 0 25 0 1 0 358529568 44425216 10269 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10846 10269 603 41 0 10805 0
vsize: 43384
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10828 0 0 0 30971 32 0 0 25 0 1 0 358529568 46428160 10750 4294967295 134512640 134672761 3221224544 3221223648 134559969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11335 10750 603 41 0 11294 0
vsize: 45340
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 31970 32 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 32970 33 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 33970 33 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 34970 33 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 35969 33 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 36969 34 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223680 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 37969 34 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 38969 34 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 39969 34 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 40969 34 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 41969 34 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223728 134558878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 42969 35 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 43969 35 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 44969 35 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 45969 35 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 46969 35 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10949 0 0 0 47969 35 0 0 25 0 1 0 358529568 46964736 10871 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10871 603 41 0 11425 0
vsize: 45864
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 48968 36 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 49968 36 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 50968 36 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 51968 36 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 52968 36 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 53968 37 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 54968 37 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 55968 37 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 56968 37 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 57968 37 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 58969 37 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 59968 37 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10950 0 0 0 60969 37 0 0 25 0 1 0 358529568 46964736 10872 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10872 603 41 0 11425 0
vsize: 45864
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10951 0 0 0 61968 37 0 0 25 0 1 0 358529568 46964736 10873 4294967295 134512640 134672761 3221224544 3221223648 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10873 603 41 0 11425 0
vsize: 45864
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 62969 37 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 63969 37 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 64969 38 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 65969 38 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 66969 38 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 67969 38 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 68969 38 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 69969 38 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 70969 38 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 71969 39 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223728 134559663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 72969 39 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223728 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 10952 0 0 0 73969 39 0 0 25 0 1 0 358529568 46964736 10874 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11466 10874 603 41 0 11425 0
vsize: 45864
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 11134 0 0 0 74968 39 0 0 25 0 1 0 358529568 47636480 11056 4294967295 134512640 134672761 3221224544 3221223648 134555114 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11630 11056 603 41 0 11589 0
vsize: 46520
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 11639 0 0 0 75967 41 0 0 25 0 1 0 358529568 49770496 11561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12151 11561 603 41 0 12110 0
vsize: 48604
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 12076 0 0 0 76966 42 0 0 25 0 1 0 358529568 51519488 11998 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12578 11998 603 41 0 12537 0
vsize: 50312
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 12521 0 0 0 77965 43 0 0 25 0 1 0 358529568 53407744 12443 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 12443 603 41 0 12998 0
vsize: 52156
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 12885 0 0 0 78964 44 0 0 25 0 1 0 358529568 54882304 12807 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13399 12807 603 41 0 13358 0
vsize: 53596
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 13272 0 0 0 79963 46 0 0 25 0 1 0 358529568 56487936 13194 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 13194 603 41 0 13750 0
vsize: 55164
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 13708 0 0 0 80961 48 0 0 25 0 1 0 358529568 58236928 13630 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14218 13630 603 41 0 14177 0
vsize: 56872
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 14137 0 0 0 81960 49 0 0 25 0 1 0 358529568 59973632 14059 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14642 14059 603 41 0 14601 0
vsize: 58568
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 14551 0 0 0 82958 51 0 0 25 0 1 0 358529568 61714432 14473 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15067 14473 603 41 0 15026 0
vsize: 60268
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 14988 0 0 0 83957 52 0 0 25 0 1 0 358529568 63442944 14910 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15489 14910 603 41 0 15448 0
vsize: 61956
[startup+850.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 15394 0 0 0 84956 53 0 0 25 0 1 0 358529568 65191936 15316 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15916 15316 603 41 0 15875 0
vsize: 63664
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 15823 0 0 0 85955 54 0 0 25 0 1 0 358529568 66920448 15745 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16338 15745 603 41 0 16297 0
vsize: 65352
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 16233 0 0 0 86954 56 0 0 25 0 1 0 358529568 68657152 16155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16762 16155 603 41 0 16721 0
vsize: 67048
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 16587 0 0 0 87953 57 0 0 25 0 1 0 358529568 70123520 16509 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17120 16509 603 41 0 17079 0
vsize: 68480
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 16950 0 0 0 88952 58 0 0 25 0 1 0 358529568 71589888 16872 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17478 16872 603 41 0 17437 0
vsize: 69912
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 17313 0 0 0 89951 59 0 0 25 0 1 0 358529568 73052160 17235 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17835 17235 603 41 0 17794 0
vsize: 71340
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 17683 0 0 0 90950 60 0 0 25 0 1 0 358529568 74510336 17605 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18191 17605 603 41 0 18150 0
vsize: 72764
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 18071 0 0 0 91948 62 0 0 25 0 1 0 358529568 76382208 17993 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18648 17993 603 41 0 18607 0
vsize: 74592
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 18519 0 0 0 92947 64 0 0 25 0 1 0 358529568 78270464 18441 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19109 18441 603 41 0 19068 0
vsize: 76436
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 18980 0 0 0 93946 65 0 0 25 0 1 0 358529568 80146432 18902 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19567 18902 603 41 0 19526 0
vsize: 78268
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 19449 0 0 0 94944 67 0 0 25 0 1 0 358529568 82018304 19371 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20024 19371 603 41 0 19983 0
vsize: 80096
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 19878 0 0 0 95943 68 0 0 25 0 1 0 358529568 83763200 19800 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20450 19800 603 41 0 20409 0
vsize: 81800
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 96942 70 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 97942 70 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 98942 70 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 99942 70 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223712 134561259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 100942 70 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 101942 71 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 102942 71 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 103941 71 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 104941 71 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 105941 71 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223700 134565028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 106941 71 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 107941 72 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 108942 72 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223680 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 109941 72 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 110941 72 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 111941 72 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 112942 72 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 113941 72 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 114941 73 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 115941 73 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 116942 73 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 117941 73 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 118942 73 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3873
Raw data (stat): 3873 (minisat+) R 3872 30927 30926 0 -1 0 20285 0 0 0 119941 73 0 0 25 0 1 0 358529568 85499904 20207 4294967295 134512640 134672761 3221224544 3221223728 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 20207 603 41 0 20833 0
vsize: 83496
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 3873
Raw data (stat): 3873 (minisat+) Z 3872 30927 30926 0 -1 12 20288 0 0 0 119941 77 0 0 25 0 1 0 358529568 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.06
CPU time (s): 1200.2
CPU user time (s): 1199.42
CPU system time (s): 0.775882
CPU usage (%): 100.011
Max. virtual memory (Kb): 83496
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####