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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos5.opb
MD5SUMe6bff154156b54af3a9a38f7579209b6
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 17324
Optimality of the best value was proved NO
Number of terms in the objective function 163
Biggest coefficient in the objective function 1024
Number of bits for the biggest coefficient in the objective function 11
Sum of the numbers in the objective function 74742
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 8192
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 74742
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.06984
Number of variables163
Total number of constraints126
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)56
Number of constraints which are nor clauses,nor cardinality constraints70
Minimum length of a constraint1
Maximum length of a constraint102

Trace number 13586

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        770484 kB
Buffers:         33072 kB
Cached:         198216 kB
SwapCached:         48 kB
Active:          38436 kB
Inactive:       195880 kB
HighTotal:      131008 kB
HighFree:         8736 kB
LowTotal:       903652 kB
LowFree:        761748 kB
SwapTotal:     2097892 kB
SwapFree:      2097840 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7032 kB
Slab:            23996 kB
Committed_AS:    63808 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 21:23:19 (client local time) WITH STATUS 10 IN 1200.48 SECONDS
stats: 14715 7 1200.48 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   10
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:  199
c ---[  61]---> BDD-cost:  363
c ---[  60]---> BDD-cost:  147
c ---[  59]---> BDD-cost:  768
c ---[  58]---> BDD-cost:  468
c ---[  57]---> BDD-cost:  147
c ---[  56]---> BDD-cost:  608
c ---[  55]---> BDD-cost:  468
c ---[  54]---> BDD-cost:  468
c ---[  53]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  608
c ---[  51]---> BDD-cost:  100
c ---[  50]---> BDD-cost:  468
c ---[  49]---> BDD-cost:  606
c ---[  48]---> BDD-cost:  250
c ---[  47]---> BDD-cost:  174
c ---[  46]---> BDD-cost:  177
c ---[  45]---> BDD-cost:  129
c ---[  44]---> BDD-cost:  176
c ---[  43]---> BDD-cost:  177
c ---[  42]---> BDD-cost:  129
c ---[  41]---> BDD-cost:  176
c ---[  40]---> BDD-cost:  171
c ---[  39]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  581
c ---[  37]---> BDD-cost:  176
c ---[  36]---> BDD-cost:  177
c ---[  35]---> BDD-cost:  129
c ---[  34]---> BDD-cost:  176
c ---[  33]---> BDD-cost:  129
c ---[  32]---> BDD-cost:  581
c ---[  31]---> BDD-cost:  177
c ---[  30]---> BDD-cost:  129
c ---[  29]---> BDD-cost:  173
c ---[  28]---> BDD-cost:  444
c ---[  27]---> BDD-cost:  581
c ---[  26]---> BDD-cost:  110
c ---[  25]---> BDD-cost:  110
c ---[  24]---> BDD-cost:  110
c ---[  23]---> BDD-cost:  150
c ---[  22]---> BDD-cost:  110
c ---[  21]---> BDD-cost:  110
c ---[  20]---> BDD-cost:  110
c ---[  19]---> BDD-cost:  150
c ---[  18]---> BDD-cost:  175
c ---[  17]---> BDD-cost:  110
c ---[  16]---> BDD-cost:  110
c ---[  15]---> BDD-cost:  150
c ---[  14]---> BDD-cost:  110
c ---[  13]---> BDD-cost:  150
c ---[  12]---> BDD-cost:  110
c ---[  11]---> BDD-cost:  418
c ---[  10]---> BDD-cost:   90
c ---[   9]---> BDD-cost:   90
c ---[   8]---> BDD-cost:   90
c ---[   7]---> BDD-cost:  175
c ---[   6]---> BDD-cost:   90
c ---[   5]---> BDD-cost:  122
c ---[   4]---> BDD-cost:   90
c ---[   3]---> BDD-cost:   69
c ---[   2]---> BDD-cost:  181
c ---[   1]---> BDD-cost:  193
c ---[   0]---> BDD-cost:  147
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38216   113117 |   12738       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 29697
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3374     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   44970   128900 |   14990       0        0     nan |  0.000 % |
c |       100 |   44970   128900 |   16489     100      596     6.0 |  0.428 % |
c |       251 |   44970   128900 |   18137     251     1549     6.2 |  0.428 % |
c ==============================================================================
c Found solution: 21963
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       450 |   45047   129099 |   15015     450     2812     6.2 |  0.428 % |
c |       550 |   45047   129099 |   16516     550     4172     7.6 |  0.433 % |
c |       700 |   45047   129099 |   18168     700     5822     8.3 |  0.433 % |
c |       925 |   45047   129099 |   19984     925     8796     9.5 |  0.433 % |
c ==============================================================================
c Found solution: 20219
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       979 |   45072   129163 |   15024     979     9148     9.3 |  0.433 % |
c |      1082 |   45072   129163 |   16526    1082    10773    10.0 |  0.438 % |
c |      1232 |   45072   129163 |   18179    1232    11901     9.7 |  0.438 % |
c |      1457 |   45072   129163 |   19996    1457    13547     9.3 |  0.438 % |
c |      1795 |   45072   129163 |   21996    1795    24684    13.8 |  0.438 % |
c |      2303 |   45072   129163 |   24196    2303    31039    13.5 |  0.438 % |
c |      3063 |   45072   129163 |   26615    3063    48131    15.7 |  0.438 % |
c |      4202 |   45072   129163 |   29277    4202    71867    17.1 |  0.438 % |
c ==============================================================================
c Found solution: 19943
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5451 |   45080   129188 |   15026    5451    86358    15.8 |  0.438 % |
c |      5551 |   45080   129188 |   16528    5551    87646    15.8 |  0.444 % |
c |      5704 |   45080   129188 |   18181    5704    89470    15.7 |  0.444 % |
c |      5929 |   45080   129188 |   19999    5929    94156    15.9 |  0.444 % |
c |      6267 |   45080   129188 |   21999    6267    97789    15.6 |  0.444 % |
c |      6773 |   45080   129188 |   24199    6773   104367    15.4 |  0.444 % |
c ==============================================================================
c Found solution: 19942
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7273 |   45108   129262 |   15036    7273   109570    15.1 |  0.444 % |
c |      7373 |   45108   129262 |   16539    7373   111221    15.1 |  0.449 % |
c |      7523 |   45108   129262 |   18193    7523   112313    14.9 |  0.449 % |
c |      7748 |   45108   129262 |   20012    7748   116589    15.0 |  0.449 % |
c |      8085 |   45108   129262 |   22014    8085   120472    14.9 |  0.449 % |
c ==============================================================================
c Found solution: 18550
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8459 |   45118   129289 |   15039    8459   129457    15.3 |  0.449 % |
c ==============================================================================
c Found solution: 18329
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8512 |   45148   129369 |   15049    8512   130576    15.3 |  0.449 % |
c |      8612 |   45142   129357 |   16553    8582   132027    15.4 |  0.477 % |
c |      8762 |   45142   129357 |   18209    8732   134291    15.4 |  0.477 % |
c |      8990 |   45142   129357 |   20030    8960   137640    15.4 |  0.477 % |
c |      9328 |   45142   129357 |   22033    9298   143509    15.4 |  0.477 % |
c |      9836 |   45142   129357 |   24236    9806   155537    15.9 |  0.477 % |
c |     10595 |   45142   129357 |   26660   10565   172988    16.4 |  0.477 % |
c |     11735 |   45142   129357 |   29326   11705   185659    15.9 |  0.477 % |
c |     13444 |   45142   129357 |   32258   13414   225240    16.8 |  0.477 % |
c |     16007 |   45142   129357 |   35484   15977   337754    21.1 |  0.477 % |
c |     19851 |   45142   129357 |   39033   19821   429705    21.7 |  0.477 % |
c ==============================================================================
c Found solution: 17910
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22838 |   45148   129377 |   15049   22808   493591    21.6 |  0.477 % |
c |     22938 |   45148   129377 |   16553   11504   278856    24.2 |  0.483 % |
c |     23089 |   45148   129377 |   18209   11655   283539    24.3 |  0.483 % |
c |     23314 |   45148   129377 |   20030   11880   289063    24.3 |  0.483 % |
c |     23651 |   45148   129377 |   22033   12217   296504    24.3 |  0.483 % |
c |     24158 |   45148   129377 |   24236   12724   312622    24.6 |  0.483 % |
c |     24917 |   45148   129377 |   26660   13483   336779    25.0 |  0.483 % |
c |     26058 |   45148   129377 |   29326   14624   360791    24.7 |  0.483 % |
c |     27766 |   45148   129377 |   32258   16332   390294    23.9 |  0.483 % |
c ==============================================================================
c Found solution: 17908
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28097 |   45156   129405 |   15052   16663   395852    23.8 |  0.483 % |
c |     28198 |   45156   129405 |   16557    8433   163786    19.4 |  0.489 % |
c |     28349 |   45156   129405 |   18212    8584   166466    19.4 |  0.489 % |
c |     28575 |   45156   129405 |   20034    8810   174167    19.8 |  0.489 % |
c |     28913 |   45156   129405 |   22037    9148   180336    19.7 |  0.489 % |
c |     29419 |   45156   129405 |   24241    9654   193330    20.0 |  0.489 % |
c |     30178 |   45154   129401 |   26665   10410   227671    21.9 |  0.494 % |
c |     31318 |   45154   129401 |   29332   11550   256723    22.2 |  0.494 % |
c |     33027 |   45154   129401 |   32265   13259   304794    23.0 |  0.494 % |
c |     35589 |   45154   129401 |   35491   15821   369487    23.4 |  0.494 % |
c |     39433 |   45154   129401 |   39041   19665   470920    23.9 |  0.494 % |
c ==============================================================================
c Found solution: 17907
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44851 |   45156   129411 |   15052   21563   494051    22.9 |  0.494 % |
c |     44951 |   45156   129411 |   16557   10806   191548    17.7 |  0.511 % |
c |     45101 |   45156   129411 |   18212   10956   194077    17.7 |  0.511 % |
c |     45326 |   45156   129411 |   20034   11181   197764    17.7 |  0.511 % |
c |     45664 |   45156   129411 |   22037   11519   207314    18.0 |  0.511 % |
c |     46170 |   45156   129411 |   24241   12025   216411    18.0 |  0.511 % |
c |     46931 |   45156   129411 |   26665   12786   230651    18.0 |  0.511 % |
c ==============================================================================
c Found solution: 17906
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47662 |   45164   129435 |   15054   13517   240957    17.8 |  0.511 % |
c |     47762 |   45164   129435 |   16559   13617   243021    17.8 |  0.517 % |
c |     47914 |   45164   129435 |   18215   13769   247263    18.0 |  0.517 % |
c |     48140 |   45164   129435 |   20036   13995   252411    18.0 |  0.517 % |
c |     48477 |   45164   129435 |   22040   14332   255755    17.8 |  0.517 % |
c |     48984 |   45164   129435 |   24244   14839   266946    18.0 |  0.517 % |
c |     49744 |   45164   129435 |   26669   15599   276261    17.7 |  0.517 % |
c |     50883 |   45164   129435 |   29335   16738   302685    18.1 |  0.517 % |
c |     52592 |   45164   129435 |   32269   18447   323906    17.6 |  0.517 % |
c ==============================================================================
c Found solution: 17881
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54227 |   45164   129438 |   15054   20070   346105    17.2 |  0.517 % |
c |     54328 |   45164   129438 |   16559   10136   133874    13.2 |  0.540 % |
c |     54480 |   45164   129438 |   18215   10288   135748    13.2 |  0.540 % |
c |     54707 |   45164   129438 |   20036   10515   139720    13.3 |  0.540 % |
c |     55045 |   45164   129438 |   22040   10853   145470    13.4 |  0.540 % |
c |     55551 |   45164   129438 |   24244   11359   157053    13.8 |  0.540 % |
c |     56310 |   45164   129438 |   26669   12118   172998    14.3 |  0.540 % |
c |     57451 |   45164   129438 |   29335   13259   217181    16.4 |  0.540 % |
c |     59159 |   45161   129431 |   32269   14735   235735    16.0 |  0.551 % |
c |     61721 |   45161   129431 |   35496   17297   289577    16.7 |  0.551 % |
c |     65566 |   45161   129431 |   39046   21142   451859    21.4 |  0.551 % |
c |     71332 |   45161   129431 |   42950   26908   626497    23.3 |  0.551 % |
c ==============================================================================
c Found solution: 17744
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73974 |   45174   129462 |   15058   29550   656185    22.2 |  0.551 % |
c |     74074 |   45174   129462 |   16563   14875   330355    22.2 |  0.557 % |
c ==============================================================================
c Found solution: 17708
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74180 |   45186   129491 |   15062   14981   332367    22.2 |  0.557 % |
c |     74281 |   45186   129491 |   16568   15082   333790    22.1 |  0.562 % |
c |     74431 |   45186   129491 |   18225   15232   337872    22.2 |  0.562 % |
c |     74657 |   45186   129491 |   20047   15458   342958    22.2 |  0.562 % |
c |     74995 |   45186   129491 |   22052   15796   351839    22.3 |  0.562 % |
c |     75503 |   45186   129491 |   24257   16304   374147    22.9 |  0.562 % |
c |     76262 |   45186   129491 |   26683   17063   403068    23.6 |  0.562 % |
c |     77403 |   45186   129491 |   29351   18204   448840    24.7 |  0.562 % |
c |     79111 |   45186   129491 |   32286   19912   527956    26.5 |  0.562 % |
c |     81673 |   45186   129491 |   35515   22474   603312    26.8 |  0.562 % |
c |     85517 |   45186   129491 |   39066   26318   719234    27.3 |  0.562 % |
c |     91283 |   45186   129491 |   42973   32084   873913    27.2 |  0.562 % |
c ==============================================================================
c Found solution: 17707
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94080 |   45195   129512 |   15065   34881   917537    26.3 |  0.562 % |
c |     94180 |   45195   129512 |   16571    8100   107641    13.3 |  0.568 % |
c |     94330 |   45195   129512 |   18228    8250   110659    13.4 |  0.568 % |
c |     94555 |   45195   129512 |   20051    8475   113822    13.4 |  0.568 % |
c |     94893 |   45195   129512 |   22056    8813   119387    13.5 |  0.568 % |
c ==============================================================================
c Found solution: 17705
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95339 |   45206   129538 |   15068    9259   126252    13.6 |  0.568 % |
c |     95439 |   45206   129538 |   16574    9359   127798    13.7 |  0.574 % |
c |     95590 |   45206   129538 |   18232    9510   129902    13.7 |  0.574 % |
c |     95816 |   45206   129538 |   20055    9736   132417    13.6 |  0.573 % |
c |     96154 |   45206   129538 |   22061   10074   138763    13.8 |  0.574 % |
c ==============================================================================
c Found solution: 17704
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96397 |   45217   129564 |   15072   10317   141901    13.8 |  0.574 % |
c |     96497 |   45217   129564 |   16579   10417   143886    13.8 |  0.579 % |
c |     96648 |   45217   129564 |   18237   10568   146385    13.9 |  0.579 % |
c |     96873 |   45217   129564 |   20060   10793   148416    13.8 |  0.579 % |
c |     97211 |   45217   129564 |   22066   11131   156231    14.0 |  0.579 % |
c |     97718 |   45217   129564 |   24273   11638   165552    14.2 |  0.579 % |
c |     98478 |   45217   129564 |   26700   12398   197214    15.9 |  0.579 % |
c |     99618 |   45217   129564 |   29371   13538   214443    15.8 |  0.579 % |
c |    101326 |   45217   129564 |   32308   15246   241163    15.8 |  0.579 % |
c |    103888 |   45217   129564 |   35538   17808   293941    16.5 |  0.579 % |
c |    107732 |   45217   129564 |   39092   21652   452320    20.9 |  0.579 % |
c ==============================================================================
c Found solution: 17670
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108763 |   45226   129584 |   15075   22683   470067    20.7 |  0.579 % |
c |    108863 |   45226   129584 |   16582   11442   249439    21.8 |  0.585 % |
c |    109014 |   45226   129584 |   18240   11593   251875    21.7 |  0.585 % |
c |    109239 |   45226   129584 |   20064   11818   258172    21.8 |  0.585 % |
c |    109576 |   45226   129584 |   22071   12155   264006    21.7 |  0.585 % |
c |    110082 |   45226   129584 |   24278   12661   272113    21.5 |  0.585 % |
c |    110841 |   45226   129584 |   26706   13420   301628    22.5 |  0.585 % |
c |    111981 |   45226   129584 |   29376   14560   353324    24.3 |  0.585 % |
c ==============================================================================
c Found solution: 17666
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113497 |   45237   129609 |   15079   16076   376343    23.4 |  0.585 % |
c |    113597 |   45235   129605 |   16586    8137   142448    17.5 |  0.596 % |
c |    113747 |   45235   129605 |   18245    8287   145023    17.5 |  0.596 % |
c |    113972 |   45235   129605 |   20070    8512   148477    17.4 |  0.596 % |
c |    114309 |   45235   129605 |   22077    8849   154191    17.4 |  0.596 % |
c |    114818 |   45235   129605 |   24284    9358   175848    18.8 |  0.596 % |
c |    115579 |   45235   129605 |   26713   10119   188714    18.6 |  0.596 % |
c |    116718 |   45235   129605 |   29384   11258   216825    19.3 |  0.596 % |
c |    118428 |   45235   129605 |   32323   12968   239716    18.5 |  0.596 % |
c |    120991 |   45235   129605 |   35555   15531   280360    18.1 |  0.596 % |
c |    124835 |   45235   129605 |   39111   19375   355471    18.3 |  0.596 % |
c |    130601 |   45235   129605 |   43022   25141   522403    20.8 |  0.596 % |
c |    139250 |   45235   129605 |   47324   33790   721872    21.4 |  0.596 % |
c ==============================================================================
c Found solution: 17665
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    139503 |   45245   129627 |   15081   34043   725424    21.3 |  0.596 % |
c |    139603 |   45245   129627 |   16589    8341   109622    13.1 |  0.602 % |
c |    139753 |   45245   129627 |   18248    8491   111234    13.1 |  0.602 % |
c |    139978 |   45245   129627 |   20072    8716   114482    13.1 |  0.602 % |
c |    140315 |   45245   129627 |   22080    9053   121179    13.4 |  0.602 % |
c ==============================================================================
c Found solution: 17664
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    140528 |   45256   129652 |   15085    9266   124871    13.5 |  0.602 % |
c |    140628 |   45256   129652 |   16593    9366   127928    13.7 |  0.607 % |
c |    140778 |   45256   129652 |   18252    9516   129663    13.6 |  0.607 % |
c |    141003 |   45256   129652 |   20078    9741   134269    13.8 |  0.607 % |
c |    141341 |   45256   129652 |   22085   10079   138173    13.7 |  0.607 % |
c |    141848 |   45256   129652 |   24294   10586   156334    14.8 |  0.607 % |
c |    142607 |   45256   129652 |   26723   11345   173302    15.3 |  0.607 % |
c ==============================================================================
c Found solution: 17591
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    143326 |   45262   129666 |   15087   12064   193899    16.1 |  0.607 % |
c |    143426 |   45262   129666 |   16595   12164   196104    16.1 |  0.613 % |
c |    143577 |   45262   129666 |   18255   12315   199946    16.2 |  0.613 % |
c |    143804 |   45262   129666 |   20080   12542   203900    16.3 |  0.613 % |
c |    144141 |   45262   129666 |   22088   12879   213936    16.6 |  0.613 % |
c |    144647 |   45262   129666 |   24297   13385   221679    16.6 |  0.613 % |
c |    145407 |   45262   129666 |   26727   14145   249299    17.6 |  0.613 % |
c |    146548 |   45262   129666 |   29400   15286   273392    17.9 |  0.613 % |
c |    148256 |   45262   129666 |   32340   16994   307763    18.1 |  0.613 % |
c ==============================================================================
c Found solution: 17590
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149001 |   45271   129688 |   15090   17739   320641    18.1 |  0.613 % |
c |    149101 |   45271   129688 |   16599    8970   135776    15.1 |  0.618 % |
c |    149252 |   45271   129688 |   18258    9121   138552    15.2 |  0.618 % |
c |    149477 |   45271   129688 |   20084    9346   141060    15.1 |  0.618 % |
c |    149814 |   45271   129688 |   22093    9683   148185    15.3 |  0.618 % |
c |    150320 |   45271   129688 |   24302   10189   155152    15.2 |  0.618 % |
c |    151079 |   45271   129688 |   26732   10948   178788    16.3 |  0.618 % |
c |    152218 |   45271   129688 |   29406   12087   198860    16.5 |  0.618 % |
c ==============================================================================
c Found solution: 17586
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    153213 |   45280   129710 |   15093   13082   214979    16.4 |  0.618 % |
c |    153313 |   45280   129710 |   16602   13182   217732    16.5 |  0.624 % |
c |    153463 |   45280   129710 |   18262   13332   220002    16.5 |  0.624 % |
c |    153689 |   45280   129710 |   20088   13558   226210    16.7 |  0.624 % |
c |    154027 |   45280   129710 |   22097   13896   235837    17.0 |  0.624 % |
c ==============================================================================
c Found solution: 17585
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    154341 |   45289   129732 |   15096   14210   241346    17.0 |  0.624 % |
c |    154441 |   45289   129732 |   16605   14310   244266    17.1 |  0.629 % |
c |    154591 |   45289   129732 |   18266   14460   247696    17.1 |  0.629 % |
c |    154816 |   45289   129732 |   20092   14685   251985    17.2 |  0.629 % |
c |    155153 |   45287   129728 |   22102   15021   254936    17.0 |  0.635 % |
c |    155659 |   45287   129728 |   24312   15527   264999    17.1 |  0.635 % |
c |    156419 |   45287   129728 |   26743   16287   275773    16.9 |  0.635 % |
c |    157558 |   45287   129728 |   29417   17426   288256    16.5 |  0.635 % |
c |    159266 |   45287   129728 |   32359   19134   331560    17.3 |  0.635 % |
c |    161828 |   45287   129728 |   35595   21696   407434    18.8 |  0.635 % |
c ==============================================================================
c Found solution: 17584
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    163924 |   45296   129749 |   15098   23792   454862    19.1 |  0.635 % |
c |    164025 |   45296   129749 |   16607   11997   198621    16.6 |  0.641 % |
c |    164176 |   45296   129749 |   18268   12148   202316    16.7 |  0.641 % |
c |    164401 |   45296   129749 |   20095   12373   205680    16.6 |  0.641 % |
c |    164738 |   45296   129749 |   22104   12710   212026    16.7 |  0.641 % |
c |    165246 |   45296   129749 |   24315   13218   230408    17.4 |  0.641 % |
c |    166006 |   45296   129749 |   26747   13978   249559    17.9 |  0.641 % |
c ==============================================================================
c Found solution: 17526
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    166765 |   45303   129764 |   15101   14737   265748    18.0 |  0.641 % |
c |    166866 |   45303   129764 |   16611   14838   268020    18.1 |  0.646 % |
c |    167016 |   45303   129764 |   18272   14988   270599    18.1 |  0.646 % |
c |    167241 |   45303   129764 |   20099   15213   273825    18.0 |  0.646 % |
c |    167578 |   45303   129764 |   22109   15550   281856    18.1 |  0.646 % |
c ==============================================================================
c Found solution: 17525
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    167931 |   45310   129784 |   15103   15903   287964    18.1 |  0.646 % |
c |    168031 |   45310   129784 |   16613    8052   104714    13.0 |  0.652 % |
c |    168181 |   45310   129784 |   18274    8202   105679    12.9 |  0.652 % |
c |    168409 |   45310   129784 |   20102    8430   108145    12.8 |  0.652 % |
c |    168750 |   45310   129784 |   22112    8771   115494    13.2 |  0.652 % |
c |    169258 |   45310   129784 |   24323    9279   130507    14.1 |  0.652 % |
c |    170017 |   45310   129784 |   26755   10038   149123    14.9 |  0.652 % |
c |    171156 |   45310   129784 |   29431   11177   163357    14.6 |  0.652 % |
c |    172864 |   45310   129784 |   32374   12885   210231    16.3 |  0.652 % |
c ==============================================================================
c Found solution: 17494
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    173207 |   45320   129807 |   15106   13228   214195    16.2 |  0.652 % |
c |    173308 |   45320   129807 |   16616   13329   216012    16.2 |  0.657 % |
c |    173458 |   45320   129807 |   18278   13479   217357    16.1 |  0.657 % |
c |    173683 |   45318   129803 |   20106   13701   219583    16.0 |  0.663 % |
c |    174020 |   45318   129803 |   22116   14038   225445    16.1 |  0.663 % |
c |    174526 |   45318   129803 |   24328   14544   230665    15.9 |  0.663 % |
c ==============================================================================
c Found solution: 17446
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175063 |   45326   129821 |   15108   15081   239249    15.9 |  0.663 % |
c |    175163 |   45326   129821 |   16618   15181   240968    15.9 |  0.669 % |
c |    175314 |   45326   129821 |   18280   15332   243534    15.9 |  0.669 % |
c |    175539 |   45326   129821 |   20108   15557   248220    16.0 |  0.669 % |
c |    175876 |   45326   129821 |   22119   15894   256913    16.2 |  0.669 % |
c |    176382 |   45326   129821 |   24331   16400   264900    16.2 |  0.669 % |
c |    177141 |   45326   129821 |   26764   17159   286459    16.7 |  0.669 % |
c ==============================================================================
c Found solution: 17445
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    177433 |   45337   129847 |   15112   17451   290547    16.6 |  0.669 % |
c |    177533 |   45337   129847 |   16623    8826    95481    10.8 |  0.674 % |
c |    177683 |   45337   129847 |   18285    8976    98347    11.0 |  0.674 % |
c |    177908 |   45337   129847 |   20114    9201   101894    11.1 |  0.674 % |
c |    178245 |   45337   129847 |   22125    9538   107326    11.3 |  0.674 % |
c |    178752 |   45337   129847 |   24338   10045   116787    11.6 |  0.674 % |
c ==============================================================================
c Found solution: 17430
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    179088 |   45344   129862 |   15114   10381   122242    11.8 |  0.674 % |
c |    179188 |   45344   129862 |   16625   10481   126796    12.1 |  0.680 % |
c |    179338 |   45344   129862 |   18287   10631   131016    12.3 |  0.680 % |
c ==============================================================================
c Found solution: 17429
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    179541 |   45353   129882 |   15117   10834   132998    12.3 |  0.680 % |
c |    179641 |   45353   129882 |   16628   10934   134549    12.3 |  0.685 % |
c |    179791 |   45353   129882 |   18291   11084   137114    12.4 |  0.685 % |
c |    180016 |   45353   129882 |   20120   11309   142304    12.6 |  0.685 % |
c |    180354 |   45353   129882 |   22132   11647   149217    12.8 |  0.685 % |
c |    180860 |   45353   129882 |   24346   12153   159113    13.1 |  0.685 % |
c ==============================================================================
c Found solution: 17428
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    181577 |   45362   129903 |   15120   12870   179956    14.0 |  0.685 % |
c |    181677 |   45362   129903 |   16632   12970   182391    14.1 |  0.691 % |
c |    181827 |   45362   129903 |   18295   13120   185776    14.2 |  0.691 % |
c |    182053 |   45362   129903 |   20124   13346   191843    14.4 |  0.691 % |
c |    182390 |   45362   129903 |   22137   13683   201566    14.7 |  0.691 % |
c |    182897 |   45362   129903 |   24350   14190   216587    15.3 |  0.691 % |
c |    183656 |   45362   129903 |   26786   14949   233329    15.6 |  0.691 % |
c |    184795 |   45362   129903 |   29464   16088   264289    16.4 |  0.691 % |
c |    186503 |   45362   129903 |   32411   17796   315662    17.7 |  0.691 % |
c ==============================================================================
c Found solution: 17427
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    186822 |   45371   129924 |   15123   18115   321510    17.7 |  0.691 % |
c |    186922 |   45371   129924 |   16635    9158   136413    14.9 |  0.697 % |
c |    187072 |   45371   129924 |   18298    9308   138870    14.9 |  0.697 % |
c |    187298 |   45371   129924 |   20128    9534   145509    15.3 |  0.697 % |
c |    187635 |   45371   129924 |   22141    9871   154695    15.7 |  0.697 % |
c |    188142 |   45371   129924 |   24355   10378   169704    16.4 |  0.697 % |
c ==============================================================================
c Found solution: 17426
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188256 |   45380   129944 |   15126   10492   171355    16.3 |  0.697 % |
c |    188356 |   45380   129944 |   16638   10592   173408    16.4 |  0.702 % |
c |    188509 |   45380   129944 |   18302   10745   176703    16.4 |  0.702 % |
c |    188735 |   45380   129944 |   20132   10971   182669    16.7 |  0.702 % |
c |    189072 |   45380   129944 |   22145   11308   188064    16.6 |  0.702 % |
c |    189579 |   45380   129944 |   24360   11815   195762    16.6 |  0.702 % |
c |    190339 |   45380   129944 |   26796   12575   209096    16.6 |  0.702 % |
c |    191482 |   45380   129944 |   29476   13718   233710    17.0 |  0.702 % |
c |    193190 |   45380   129944 |   32423   15426   263074    17.1 |  0.702 % |
c |    195752 |   45380   129944 |   35666   17988   333864    18.6 |  0.702 % |
c ==============================================================================
c Found solution: 17425
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    196158 |   45389   129964 |   15129   18394   340225    18.5 |  0.702 % |
c |    196258 |   45389   129964 |   16641    9297   128447    13.8 |  0.708 % |
c |    196408 |   45389   129964 |   18306    9447   132555    14.0 |  0.708 % |
c |    196633 |   45389   129964 |   20136    9672   137237    14.2 |  0.708 % |
c |    196971 |   45389   129964 |   22150   10010   145208    14.5 |  0.708 % |
c |    197478 |   45389   129964 |   24365   10517   155366    14.8 |  0.708 % |
c |    198237 |   45389   129964 |   26801   11276   173759    15.4 |  0.708 % |
c |    199377 |   45389   129964 |   29482   12416   192821    15.5 |  0.708 % |
c |    201085 |   45389   129964 |   32430   14124   226614    16.0 |  0.708 % |
c |    203649 |   45389   129964 |   35673   16688   287311    17.2 |  0.708 % |
c ==============================================================================
c Found solution: 17422
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    205292 |   45401   129991 |   15133   18331   343530    18.7 |  0.708 % |
c |    205392 |   45401   129991 |   16646    9266   143788    15.5 |  0.713 % |
c |    205542 |   45401   129991 |   18310    9416   145392    15.4 |  0.713 % |
c |    205768 |   45401   129991 |   20142    9642   148989    15.5 |  0.713 % |
c |    206105 |   45401   129991 |   22156    9979   155217    15.6 |  0.713 % |
c |    206611 |   45401   129991 |   24371   10485   168291    16.1 |  0.713 % |
c |    207370 |   45401   129991 |   26809   11244   182328    16.2 |  0.713 % |
c ==============================================================================
c Found solution: 16390
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207976 |   45409   130011 |   15136   11850   199471    16.8 |  0.713 % |
c |    208077 |   45409   130011 |   16649   11951   201946    16.9 |  0.719 % |
c |    208227 |   45409   130011 |   18314   12101   204961    16.9 |  0.719 % |
c |    208452 |   45409   130011 |   20146   12326   209392    17.0 |  0.719 % |
c |    208790 |   45409   130011 |   22160   12664   218390    17.2 |  0.719 % |
c |    209297 |   45409   130011 |   24376   13171   225716    17.1 |  0.719 % |
c |    210056 |   45409   130011 |   26814   13930   244150    17.5 |  0.719 % |
c |    211195 |   45409   130011 |   29495   15069   276080    18.3 |  0.719 % |
c |    212904 |   45409   130011 |   32445   16778   325749    19.4 |  0.719 % |
c ==============================================================================
c Found solution: 16386
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    214943 |   45414   130022 |   15138   18817   362124    19.2 |  0.719 % |
c |    215043 |   45414   130022 |   16651    9509   131383    13.8 |  0.724 % |
c |    215193 |   45414   130022 |   18316    9659   135268    14.0 |  0.724 % |
c |    215419 |   45414   130022 |   20148    9885   139858    14.1 |  0.724 % |
c |    215756 |   45414   130022 |   22163   10222   150133    14.7 |  0.724 % |
c |    216264 |   45414   130022 |   24379   10730   164196    15.3 |  0.724 % |
c |    217026 |   45414   130022 |   26817   11492   180266    15.7 |  0.724 % |
c |    218166 |   45414   130022 |   29499   12632   195116    15.4 |  0.724 % |
c |    219874 |   45414   130022 |   32449   14340   243475    17.0 |  0.724 % |
c ==============================================================================
c Found solution: 16385
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    221263 |   45420   130035 |   15140   15729   302709    19.2 |  0.724 % |
c |    221367 |   45420   130035 |   16654    7969   132837    16.7 |  0.730 % |
c |    221518 |   45420   130035 |   18319    8120   136244    16.8 |  0.730 % |
c |    221745 |   45420   130035 |   20151    8347   143499    17.2 |  0.730 % |
c |    222084 |   45420   130035 |   22166    8686   151348    17.4 |  0.730 % |
c |    222591 |   45420   130035 |   24383    9193   164491    17.9 |  0.730 % |
c |    223351 |   45420   130035 |   26821    9953   186282    18.7 |  0.730 % |
c |    224490 |   45420   130035 |   29503   11092   208715    18.8 |  0.730 % |
c |    226199 |   45420   130035 |   32453   12801   260651    20.4 |  0.730 % |
c |    228761 |   45420   130035 |   35699   15363   321071    20.9 |  0.730 % |
c |    232606 |   45420   130035 |   39269   19208   530660    27.6 |  0.730 % |
c |    238372 |   45420   130035 |   43196   24974   614466    24.6 |  0.730 % |
c |    247022 |   45411   130016 |   47515   33618   958943    28.5 |  0.759 % |
c |    259996 |   45411   130016 |   52267   46592  1403324    30.1 |  0.759 % |
c ==============================================================================
c Found solution: 16384
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    276964 |   45416   130027 |   15138   28788   924703    32.1 |  0.759 % |
c |    277066 |   45416   130027 |   16651   14496   431943    29.8 |  0.764 % |
c |    277216 |   45416   130027 |   18316   14646   434769    29.7 |  0.764 % |
c |    277441 |   45416   130027 |   20148   14871   439986    29.6 |  0.764 % |
c |    277779 |   45416   130027 |   22163   15209   442704    29.1 |  0.764 % |
c |    278286 |   45416   130027 |   24379   15716   453389    28.8 |  0.764 % |
c |    279045 |   45416   130027 |   26817   16475   465559    28.3 |  0.764 % |
c |    280184 |   45416   130027 |   29499   17614   493455    28.0 |  0.764 % |
c |    281892 |   45416   130027 |   32449   19322   555797    28.8 |  0.764 % |
c |    284454 |   45416   130027 |   35694   21884   650442    29.7 |  0.764 % |
c |    288298 |   45416   130027 |   39264   25728   850219    33.0 |  0.764 % |
c |    294064 |   45416   130027 |   43190   31494  1089927    34.6 |  0.764 % |
c |    302713 |   45416   130027 |   47509   40143  1450889    36.1 |  0.764 % |
c |    315689 |   45416   130027 |   52260   23375   631232    27.0 |  0.764 % |
c ==============================================================================
c Found solution: 16333
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    329262 |   45434   130073 |   15144   36948  1669939    45.2 |  0.764 % |
c |    329365 |   45434   130073 |   16658    8441   468180    55.5 |  0.786 % |
c |    329517 |   45434   130073 |   18324    8593   471798    54.9 |  0.786 % |
c |    329743 |   45434   130073 |   20156    8819   477245    54.1 |  0.786 % |
c |    330081 |   45434   130073 |   22172    9157   484368    52.9 |  0.786 % |
c |    330587 |   45434   130073 |   24389    9663   496174    51.3 |  0.786 % |
c |    331346 |   45434   130073 |   26828   10422   516398    49.5 |  0.786 % |
c |    332485 |   45434   130073 |   29511   11561   544250    47.1 |  0.786 % |
c |    334193 |   45434   130073 |   32462   13269   602950    45.4 |  0.786 % |
c |    336756 |   45434   130073 |   35708   15832   678476    42.9 |  0.786 % |
c |    340602 |   45434   130073 |   39279   19678   809481    41.1 |  0.786 % |
c |    346368 |   45434   130073 |   43207   25444   977814    38.4 |  0.786 % |
c |    355019 |   45434   130073 |   47528   34095  1346596    39.5 |  0.786 % |
c |    367995 |   45434   130073 |   52281   47071  1869611    39.7 |  0.786 % |
c |    387457 |   45434   130073 |   57509   32553   988593    30.4 |  0.786 % |
c |    416649 |   45434   130073 |   63260   21643   507948    23.5 |  0.786 % |
c ==============================================================================
c Found solution: 16118
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    459125 |   45442   130094 |   15147   64119  2195192    34.2 |  0.786 % |
c |    459227 |   45442   130094 |   16661    9929   219902    22.1 |  0.792 % |
c |    459377 |   45442   130094 |   18327   10079   224220    22.2 |  0.792 % |
c |    459602 |   45442   130094 |   20160   10304   230028    22.3 |  0.792 % |
c |    459939 |   45442   130094 |   22176   10641   241843    22.7 |  0.792 % |
c |    460446 |   45442   130094 |   24394   11148   259194    23.3 |  0.792 % |
c |    461205 |   45442   130094 |   26833   11907   280344    23.5 |  0.792 % |
c |    462344 |   45442   130094 |   29517   13046   318586    24.4 |  0.792 % |
c |    464053 |   45442   130094 |   32468   14755   376570    25.5 |  0.792 % |
c |    466615 |   45442   130094 |   35715   17317   467468    27.0 |  0.792 % |
c |    470460 |   45442   130094 |   39287   21162   616474    29.1 |  0.792 % |
c |    476228 |   45442   130094 |   43216   26930   840213    31.2 |  0.792 % |
c |    484879 |   45442   130094 |   47537   35581  1198988    33.7 |  0.792 % |
c |    497853 |   45442   130094 |   52291   18763   578014    30.8 |  0.792 % |
c |    517316 |   45442   130094 |   57520   38226  1367300    35.8 |  0.792 % |
c |    546510 |   45442   130094 |   63272   29077   944571    32.5 |  0.792 % |
c |    590301 |   45442   130094 |   69600   29740   936634    31.5 |  0.792 % |
c |    655986 |   45442   130094 |   76560   47036  1551733    33.0 |  0.792 % |
c ==============================================================================
c Found solution: 16115
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    695134 |   45449   130113 |   15149   25950  1109611    42.8 |  0.792 % |
c |    695235 |   45449   130113 |   16663   13076   383986    29.4 |  0.797 % |
c |    695387 |   45449   130113 |   18330   13228   385208    29.1 |  0.797 % |
c |    695612 |   45449   130113 |   20163   13453   387240    28.8 |  0.797 % |
c |    695949 |   45449   130113 |   22179   13790   390894    28.3 |  0.797 % |
c |    696455 |   45449   130113 |   24397   14296   402721    28.2 |  0.797 % |
c |    697214 |   45449   130113 |   26837   15055   428611    28.5 |  0.797 % |
c |    698353 |   45449   130113 |   29521   16194   463269    28.6 |  0.797 % |
c |    700061 |   45449   130113 |   32473   17902   511684    28.6 |  0.797 % |
c |    702624 |   45449   130113 |   35720   20465   587691    28.7 |  0.797 % |
c |    706468 |   45449   130113 |   39292   24309   723802    29.8 |  0.797 % |
c |    712234 |   45449   130113 |   43221   30075   910355    30.3 |  0.797 % |
c |    720883 |   45449   130113 |   47544   38724  1193104    30.8 |  0.797 % |
c ==============================================================================
c Found solution: 16114
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    730427 |   45456   130131 |   15152   48268  1482551    30.7 |  0.797 % |
c |    730527 |   45456   130131 |   16667    8762   115223    13.2 |  0.803 % |
c |    730677 |   45456   130131 |   18333    8912   118418    13.3 |  0.803 % |
c |    730903 |   45456   130131 |   20167    9138   124304    13.6 |  0.803 % |
c |    731240 |   45456   130131 |   22184    9475   131690    13.9 |  0.803 % |
c |    731746 |   45456   130131 |   24402    9981   145132    14.5 |  0.803 % |
c |    732505 |   45456   130131 |   26842   10740   167390    15.6 |  0.803 % |
c |    733644 |   45456   130131 |   29526   11879   201857    17.0 |  0.803 % |
c |    735353 |   45456   130131 |   32479   13588   253888    18.7 |  0.803 % |
c |    737915 |   45456   130131 |   35727   16150   333515    20.7 |  0.803 % |
c |    741759 |   45456   130131 |   39300   19994   451995    22.6 |  0.803 % |
c |    747526 |   45456   130131 |   43230   25761   632647    24.6 |  0.803 % |
c |    756176 |   45456   130131 |   47553   34411  1045292    30.4 |  0.803 % |
c |    769151 |   45456   130131 |   52308   47386  1633754    34.5 |  0.803 % |
c |    788614 |   45456   130131 |   57539   32322   970970    30.0 |  0.803 % |
c ==============================================================================
c Found solution: 16106
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    813879 |   45465   130155 |   15155   57587  2028556    35.2 |  0.803 % |
c |    813979 |   45465   130155 |   16670    8829   169193    19.2 |  0.808 % |
c |    814130 |   45465   130155 |   18337    8980   171065    19.0 |  0.808 % |
c |    814355 |   45465   130155 |   20171    9205   175061    19.0 |  0.808 % |
c |    814692 |   45465   130155 |   22188    9542   181094    19.0 |  0.808 % |
c |    815200 |   45465   130155 |   24407   10050   190585    19.0 |  0.808 % |
c |    815960 |   45465   130155 |   26848   10810   206527    19.1 |  0.808 % |
c |    817100 |   45465   130155 |   29532   11950   226939    19.0 |  0.808 % |
c |    818808 |   45465   130155 |   32486   13658   259149    19.0 |  0.808 % |
c |    821370 |   45465   130155 |   35734   16220   301543    18.6 |  0.808 % |
c |    825214 |   45465   130155 |   39308   20064   365377    18.2 |  0.808 % |
c |    830982 |   45459   130142 |   43238   25827   515423    20.0 |  0.819 % |
c |    839632 |   45459   130142 |   47562   34477   805724    23.4 |  0.819 % |
c |    852606 |   45459   130142 |   52319   47451  1286882    27.1 |  0.819 % |
c ==============================================================================
c Found solution: 16104
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    869468 |   45466   130160 |   15155   25565   995028    38.9 |  0.819 % |
#### 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.90 0.96 0.86 2/55 15796
Raw data (stat): 15796 (runsolver) R 15795 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539537392 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0001 s]
Raw data (loadavg): 0.91 0.96 0.86 2/55 15796
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2257 0 0 0 994 5 0 0 25 0 1 0 539537392 12034048 2230 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2938 2230 603 41 0 2897 0
vsize: 11752
[startup+20.0006 s]
Raw data (loadavg): 0.92 0.96 0.86 2/55 15796
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2485 0 0 0 1993 5 0 0 25 0 1 0 539537392 12906496 2458 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3151 2458 603 41 0 3110 0
vsize: 12604
[startup+30.0012 s]
Raw data (loadavg): 0.94 0.96 0.87 2/55 15796
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2604 0 0 0 2992 5 0 0 25 0 1 0 539537392 13447168 2577 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3283 2577 603 41 0 3242 0
vsize: 13132
[startup+40.0009 s]
Raw data (loadavg): 0.94 0.96 0.87 2/55 15796
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2632 0 0 0 3992 6 0 0 25 0 1 0 539537392 13578240 2605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3315 2605 603 41 0 3274 0
vsize: 13260
[startup+50.0001 s]
Raw data (loadavg): 0.95 0.96 0.87 2/55 15796
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2705 0 0 0 4992 6 0 0 25 0 1 0 539537392 13848576 2678 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2678 603 41 0 3340 0
vsize: 13524
[startup+60.0004 s]
Raw data (loadavg): 0.96 0.96 0.87 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 2852 0 0 0 5991 7 0 0 25 0 1 0 539537392 14397440 2825 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3515 2825 603 41 0 3474 0
vsize: 14060
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.96 0.87 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3078 0 0 0 6990 8 0 0 25 0 1 0 539537392 15331328 3051 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3743 3051 603 41 0 3702 0
vsize: 14972
[startup+80.0015 s]
Raw data (loadavg): 0.97 0.96 0.87 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 7989 9 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3170 603 41 0 3862 0
vsize: 15612
[startup+90.0021 s]
Raw data (loadavg): 0.97 0.96 0.87 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 8989 9 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3170 603 41 0 3862 0
vsize: 15612
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.87 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 9989 10 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3170 603 41 0 3862 0
vsize: 15612
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.87 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 10989 10 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3170 603 41 0 3862 0
vsize: 15612
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.87 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 11988 10 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3170 603 41 0 3862 0
vsize: 15612
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 12988 10 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3170 603 41 0 3862 0
vsize: 15612
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15798
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 13988 11 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223552 1075349719 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3170 603 41 0 3862 0
vsize: 15612
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3197 0 0 0 14987 12 0 0 25 0 1 0 539537392 15986688 3170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3170 603 41 0 3862 0
vsize: 15612
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3198 0 0 0 15987 12 0 0 25 0 1 0 539537392 15986688 3171 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3171 603 41 0 3862 0
vsize: 15612
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3198 0 0 0 16987 12 0 0 25 0 1 0 539537392 15986688 3171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3171 603 41 0 3862 0
vsize: 15612
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3198 0 0 0 17987 13 0 0 25 0 1 0 539537392 15986688 3171 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3171 603 41 0 3862 0
vsize: 15612
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3478 0 0 0 18986 14 0 0 25 0 1 0 539537392 17063936 3451 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3451 603 41 0 4125 0
vsize: 16664
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 3845 0 0 0 19983 16 0 0 25 0 1 0 539537392 18522112 3818 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4522 3818 603 41 0 4481 0
vsize: 18088
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4233 0 0 0 20983 17 0 0 25 0 1 0 539537392 20156416 4206 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4921 4206 603 41 0 4880 0
vsize: 19684
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 21983 18 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4342 603 41 0 5011 0
vsize: 20208
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 22983 18 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4342 603 41 0 5011 0
vsize: 20208
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 23983 18 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4342 603 41 0 5011 0
vsize: 20208
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 24983 18 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4342 603 41 0 5011 0
vsize: 20208
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 25982 19 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4342 603 41 0 5011 0
vsize: 20208
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4369 0 0 0 26982 19 0 0 25 0 1 0 539537392 20692992 4342 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5052 4342 603 41 0 5011 0
vsize: 20208
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4491 0 0 0 27982 20 0 0 25 0 1 0 539537392 21233664 4464 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5184 4464 603 41 0 5143 0
vsize: 20736
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4499 0 0 0 28981 20 0 0 25 0 1 0 539537392 21233664 4472 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5184 4472 603 41 0 5143 0
vsize: 20736
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4499 0 0 0 29981 20 0 0 25 0 1 0 539537392 21233664 4472 4294967295 134512640 134672761 3221224544 3221223680 134565039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5184 4472 603 41 0 5143 0
vsize: 20736
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4506 0 0 0 30982 20 0 0 25 0 1 0 539537392 21233664 4479 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5184 4479 603 41 0 5143 0
vsize: 20736
[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4506 0 0 0 31982 21 0 0 25 0 1 0 539537392 21233664 4479 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5184 4479 603 41 0 5143 0
vsize: 20736
[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4506 0 0 0 32983 21 0 0 25 0 1 0 539537392 21233664 4479 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5184 4479 603 41 0 5143 0
vsize: 20736
[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4506 0 0 0 33983 21 0 0 25 0 1 0 539537392 21233664 4479 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5184 4479 603 41 0 5143 0
vsize: 20736
[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15800
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4826 0 0 0 34982 22 0 0 25 0 1 0 539537392 22564864 4799 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5509 4799 603 41 0 5468 0
vsize: 22036
[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4944 0 0 0 35981 23 0 0 25 0 1 0 539537392 23101440 4917 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5640 4917 603 41 0 5599 0
vsize: 22560
[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4944 0 0 0 36980 23 0 0 25 0 1 0 539537392 23101440 4917 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5640 4917 603 41 0 5599 0
vsize: 22560
[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 4967 0 0 0 37980 24 0 0 25 0 1 0 539537392 23240704 4940 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5674 4940 603 41 0 5633 0
vsize: 22696
[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5006 0 0 0 38980 24 0 0 25 0 1 0 539537392 23404544 4979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5714 4979 603 41 0 5673 0
vsize: 22856
[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5062 0 0 0 39979 25 0 0 25 0 1 0 539537392 23764992 5035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5802 5035 603 41 0 5761 0
vsize: 23208
[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5062 0 0 0 40979 25 0 0 25 0 1 0 539537392 23764992 5035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5802 5035 603 41 0 5761 0
vsize: 23208
[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5062 0 0 0 41979 25 0 0 25 0 1 0 539537392 23764992 5035 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5802 5035 603 41 0 5761 0
vsize: 23208
[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5063 0 0 0 42979 26 0 0 25 0 1 0 539537392 23764992 5036 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5802 5036 603 41 0 5761 0
vsize: 23208
[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5077 0 0 0 43979 26 0 0 25 0 1 0 539537392 23764992 5050 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5802 5050 603 41 0 5761 0
vsize: 23208
[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5092 0 0 0 44978 26 0 0 25 0 1 0 539537392 23764992 5065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5802 5065 603 41 0 5761 0
vsize: 23208
[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5338 0 0 0 45977 27 0 0 25 0 1 0 539537392 24825856 5311 4294967295 134512640 134672761 3221224544 3221223648 134554647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6061 5311 603 41 0 6020 0
vsize: 24244
[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5338 0 0 0 46977 27 0 0 25 0 1 0 539537392 24825856 5311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6061 5311 603 41 0 6020 0
vsize: 24244
[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5338 0 0 0 47977 28 0 0 25 0 1 0 539537392 24825856 5311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6061 5311 603 41 0 6020 0
vsize: 24244
[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5341 0 0 0 48977 28 0 0 25 0 1 0 539537392 24825856 5314 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6061 5314 603 41 0 6020 0
vsize: 24244
[startup+500.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5360 0 0 0 49977 29 0 0 25 0 1 0 539537392 24961024 5333 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6094 5333 603 41 0 6053 0
vsize: 24376
[startup+510.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5371 0 0 0 50976 29 0 0 25 0 1 0 539537392 24961024 5344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6094 5344 603 41 0 6053 0
vsize: 24376
[startup+520.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5381 0 0 0 51976 29 0 0 25 0 1 0 539537392 25157632 5354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6142 5354 603 41 0 6101 0
vsize: 24568
[startup+530.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5389 0 0 0 52977 30 0 0 25 0 1 0 539537392 25157632 5362 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6142 5362 603 41 0 6101 0
vsize: 24568
[startup+540.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5402 0 0 0 53976 31 0 0 25 0 1 0 539537392 25157632 5375 4294967295 134512640 134672761 3221224544 3221223728 134558941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6142 5375 603 41 0 6101 0
vsize: 24568
[startup+550.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5406 0 0 0 54976 31 0 0 25 0 1 0 539537392 25157632 5379 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6142 5379 603 41 0 6101 0
vsize: 24568
[startup+560.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5407 0 0 0 55976 31 0 0 25 0 1 0 539537392 25157632 5380 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6142 5380 603 41 0 6101 0
vsize: 24568
[startup+570.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5433 0 0 0 56976 32 0 0 25 0 1 0 539537392 25354240 5406 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6190 5406 603 41 0 6149 0
vsize: 24760
[startup+580.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5435 0 0 0 57976 32 0 0 25 0 1 0 539537392 25354240 5408 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6190 5408 603 41 0 6149 0
vsize: 24760
[startup+590.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5437 0 0 0 58975 32 0 0 25 0 1 0 539537392 25354240 5410 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6190 5410 603 41 0 6149 0
vsize: 24760
[startup+600.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5472 0 0 0 59975 33 0 0 25 0 1 0 539537392 25550848 5445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6238 5445 603 41 0 6197 0
vsize: 24952
[startup+610.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5536 0 0 0 60975 33 0 0 25 0 1 0 539537392 25681920 5509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5509 603 41 0 6229 0
vsize: 25080
[startup+620.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5594 0 0 0 61974 34 0 0 25 0 1 0 539537392 25944064 5567 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6334 5567 603 41 0 6293 0
vsize: 25336
[startup+630.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5608 0 0 0 62974 34 0 0 25 0 1 0 539537392 26116096 5581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6376 5581 603 41 0 6335 0
vsize: 25504
[startup+640.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5637 0 0 0 63974 34 0 0 25 0 1 0 539537392 26116096 5610 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6376 5610 603 41 0 6335 0
vsize: 25504
[startup+650.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15802
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5639 0 0 0 64974 34 0 0 25 0 1 0 539537392 26116096 5612 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6376 5612 603 41 0 6335 0
vsize: 25504
[startup+660.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5659 0 0 0 65973 35 0 0 25 0 1 0 539537392 26312704 5632 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6424 5632 603 41 0 6383 0
vsize: 25696
[startup+670.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5661 0 0 0 66973 35 0 0 25 0 1 0 539537392 26312704 5634 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6424 5634 603 41 0 6383 0
vsize: 25696
[startup+680.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5662 0 0 0 67973 35 0 0 25 0 1 0 539537392 26312704 5635 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6424 5635 603 41 0 6383 0
vsize: 25696
[startup+690.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5662 0 0 0 68973 36 0 0 25 0 1 0 539537392 26312704 5635 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6424 5635 603 41 0 6383 0
vsize: 25696
[startup+700.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5692 0 0 0 69973 36 0 0 25 0 1 0 539537392 26509312 5665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6472 5665 603 41 0 6431 0
vsize: 25888
[startup+710.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5714 0 0 0 70973 36 0 0 25 0 1 0 539537392 26705920 5687 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6520 5687 603 41 0 6479 0
vsize: 26080
[startup+720.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5751 0 0 0 71973 36 0 0 25 0 1 0 539537392 26841088 5724 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6553 5724 603 41 0 6512 0
vsize: 26212
[startup+730.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5751 0 0 0 72973 36 0 0 25 0 1 0 539537392 26841088 5724 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6553 5724 603 41 0 6512 0
vsize: 26212
[startup+740.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5754 0 0 0 73973 36 0 0 25 0 1 0 539537392 26841088 5727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6553 5727 603 41 0 6512 0
vsize: 26212
[startup+750.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5761 0 0 0 74972 37 0 0 25 0 1 0 539537392 26841088 5734 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6553 5734 603 41 0 6512 0
vsize: 26212
[startup+760.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5778 0 0 0 75973 37 0 0 25 0 1 0 539537392 27021312 5751 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6597 5751 603 41 0 6556 0
vsize: 26388
[startup+770.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5784 0 0 0 76974 38 0 0 25 0 1 0 539537392 27021312 5757 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6597 5757 603 41 0 6556 0
vsize: 26388
[startup+780.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5806 0 0 0 77974 38 0 0 25 0 1 0 539537392 27021312 5779 4294967295 134512640 134672761 3221224544 3221223728 134558880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6597 5779 603 41 0 6556 0
vsize: 26388
[startup+790.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5808 0 0 0 78977 39 0 0 25 0 1 0 539537392 27021312 5781 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6597 5781 603 41 0 6556 0
vsize: 26388
[startup+800.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5809 0 0 0 79976 39 0 0 25 0 1 0 539537392 27021312 5782 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6597 5782 603 41 0 6556 0
vsize: 26388
[startup+810.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5836 0 0 0 80977 39 0 0 25 0 1 0 539537392 27283456 5809 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6661 5809 603 41 0 6620 0
vsize: 26644
[startup+820.341 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 5866 0 0 0 81997 39 0 0 25 0 1 0 539537392 27283456 5839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6661 5839 603 41 0 6620 0
vsize: 26644
[startup+830.342 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6010 0 0 0 82997 40 0 0 25 0 1 0 539537392 28078080 5983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6855 5983 603 41 0 6814 0
vsize: 27420
[startup+840.342 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6138 0 0 0 83996 41 0 0 25 0 1 0 539537392 28741632 6111 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7017 6111 603 41 0 6976 0
vsize: 28068
[startup+850.346 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6140 0 0 0 84996 41 0 0 25 0 1 0 539537392 28741632 6113 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7017 6113 603 41 0 6976 0
vsize: 28068
[startup+860.346 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6140 0 0 0 85996 41 0 0 25 0 1 0 539537392 28741632 6113 4294967295 134512640 134672761 3221224544 3221223728 134559055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7017 6113 603 41 0 6976 0
vsize: 28068
[startup+870.346 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6146 0 0 0 86995 42 0 0 25 0 1 0 539537392 28741632 6119 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7017 6119 603 41 0 6976 0
vsize: 28068
[startup+880.376 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6152 0 0 0 87998 42 0 0 25 0 1 0 539537392 28741632 6125 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7017 6125 603 41 0 6976 0
vsize: 28068
[startup+890.376 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6153 0 0 0 88999 42 0 0 25 0 1 0 539537392 28741632 6126 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7017 6126 603 41 0 6976 0
vsize: 28068
[startup+900.377 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6171 0 0 0 89998 42 0 0 25 0 1 0 539537392 29003776 6144 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7081 6144 603 41 0 7040 0
vsize: 28324
[startup+910.378 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6198 0 0 0 90989 43 0 0 25 0 1 0 539537392 29003776 6171 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7081 6171 603 41 0 7040 0
vsize: 28324
[startup+920.379 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6198 0 0 0 91989 43 0 0 25 0 1 0 539537392 29003776 6171 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7081 6171 603 41 0 7040 0
vsize: 28324
[startup+930.379 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6198 0 0 0 92989 43 0 0 25 0 1 0 539537392 29003776 6171 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7081 6171 603 41 0 7040 0
vsize: 28324
[startup+940.379 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6495 0 0 0 93988 44 0 0 25 0 1 0 539537392 30220288 6468 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7378 6468 603 41 0 7337 0
vsize: 29512
[startup+950.38 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15804
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6757 0 0 0 94987 46 0 0 25 0 1 0 539537392 31289344 6730 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7639 6730 603 41 0 7598 0
vsize: 30556
[startup+960.38 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6758 0 0 0 95987 46 0 0 25 0 1 0 539537392 31289344 6731 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7639 6731 603 41 0 7598 0
vsize: 30556
[startup+970.379 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6758 0 0 0 96986 47 0 0 25 0 1 0 539537392 31289344 6731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7639 6731 603 41 0 7598 0
vsize: 30556
[startup+980.387 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6758 0 0 0 97987 47 0 0 25 0 1 0 539537392 31289344 6731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7639 6731 603 41 0 7598 0
vsize: 30556
[startup+990.387 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6758 0 0 0 98986 48 0 0 25 0 1 0 539537392 31289344 6731 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7639 6731 603 41 0 7598 0
vsize: 30556
[startup+1000.39 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 99986 48 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6746 603 41 0 7640 0
vsize: 30724
[startup+1010.39 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 100986 48 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6746 603 41 0 7640 0
vsize: 30724
[startup+1020.4 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 101987 48 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6746 603 41 0 7640 0
vsize: 30724
[startup+1030.42 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 102989 48 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6746 603 41 0 7640 0
vsize: 30724
[startup+1040.42 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6773 0 0 0 103989 49 0 0 25 0 1 0 539537392 31461376 6746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6746 603 41 0 7640 0
vsize: 30724
[startup+1050.43 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6774 0 0 0 104990 49 0 0 25 0 1 0 539537392 31461376 6747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6747 603 41 0 7640 0
vsize: 30724
[startup+1060.43 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6777 0 0 0 105990 49 0 0 25 0 1 0 539537392 31461376 6750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6750 603 41 0 7640 0
vsize: 30724
[startup+1070.45 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6792 0 0 0 106990 50 0 0 25 0 1 0 539537392 31461376 6765 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6765 603 41 0 7640 0
vsize: 30724
[startup+1080.45 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 107990 50 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223500 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1090.45 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 108990 50 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1100.46 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 109991 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1110.47 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 110991 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1120.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 111993 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1130.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 112993 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1140.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 113993 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1150.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 114993 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1160.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 115994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1170.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 116994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1180.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 117994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1190.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 118994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
[startup+1200.49 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15806
Raw data (stat): 15796 (minisat+) R 15795 20838 20837 0 -1 0 6809 0 0 0 119994 51 0 0 25 0 1 0 539537392 31657984 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6782 603 41 0 7688 0
vsize: 30916
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.51 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 15806
Raw data (stat): 15796 (minisat+) Z 15795 20838 20837 0 -1 12 6812 0 0 0 119995 52 0 0 25 0 1 0 539537392 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.51
CPU time (s): 1200.48
CPU user time (s): 1199.95
CPU system time (s): 0.526919
CPU usage (%): 99.9975
Max. virtual memory (Kb): 30916
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####