PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0201.opb
MD5SUM	ffa3a55eb53181880328dd1b84f91e66
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1523
Optimality of the best value was proved	NO
Number of terms in the objective function	201
Biggest coefficient in the objective function	1920
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	19980
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	1920
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	19980
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02284
Number of variables	201
Total number of constraints	334
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	227
Number of constraints which are nor clauses,nor cardinality constraints	87
Minimum length of a constraint	1
Maximum length of a constraint	67
Trace number 22069

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        638624 kB
Buffers:         27584 kB
Cached:         347004 kB
SwapCached:        432 kB
Active:          40884 kB
Inactive:       335912 kB
HighTotal:      131008 kB
HighFree:        60564 kB
LowTotal:       903652 kB
LowFree:        578060 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5364 kB
Slab:            13528 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:23:34 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 12129 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 133 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): sssss
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   15
c ---[ 113]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   15
c ---[ 107]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   39
c ---[  88]---> BDD-cost:   42
c ---[  87]---> BDD-cost:   42
c ---[  86]---> BDD-cost:   54
c ---[  85]---> BDD-cost:   73
c ---[  84]---> BDD-cost:   73
c ---[  83]---> BDD-cost:   98
c ---[  82]---> BDD-cost:   85
c ---[  81]---> BDD-cost:   85
c ---[  80]---> BDD-cost:  160
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  201
c ---[  76]---> BDD-cost:  128
c ---[  75]---> BDD-cost:  128
c ---[  74]---> BDD-cost:  241
c ---[  73]---> BDD-cost:  150
c ---[  72]---> BDD-cost:  150
c ---[  71]---> BDD-cost:  281
c ---[  70]---> BDD-cost:  172
c ---[  69]---> BDD-cost:  172
c ---[  68]---> BDD-cost:  321
c ---[  67]---> BDD-cost:  194
c ---[  66]---> BDD-cost:  194
c ---[  65]---> BDD-cost:  361
c ---[  64]---> BDD-cost:    3
c ---[  63]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   11
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   11
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   11
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23540    68455 |    7846       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 2734[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:21097     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         7 |   78351   196805 |   26117       3       60    20.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2329[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       106 |   77002   193861 |   25667      84     1079    12.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       118 |   77013   193888 |   25671      96     1193    12.4 |  0.000 % |
c |       218 |   76399   192474 |   28238     185     3409    18.4 |  4.161 % |
c |       368 |   75394   190171 |   31061     323     4790    14.8 |  5.253 % |
c |       594 |   71969   182251 |   34168     514     8965    17.4 |  9.788 % |
c ==============================================================================
c [1mFound solution: 2283[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       822 |   71047   180141 |   23682     720    13788    19.1 |  9.788 % |
c |       922 |   70655   179234 |   26050     817    14502    17.8 | 11.766 % |
c |      1072 |   70585   179073 |   28655     965    17039    17.7 | 11.866 % |
c |      1300 |   70578   179052 |   31520    1190    21713    18.2 | 11.871 % |
c ==============================================================================
c [1mFound solution: 2225[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1454 |   70707   179370 |   23569    1344    24163    18.0 | 11.871 % |
c ==============================================================================
c [1mFound solution: 2191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1457 |   70723   179410 |   23574    1347    24215    18.0 | 11.871 % |
c |      1557 |   70723   179410 |   25931    1447    26069    18.0 | 11.918 % |
c |      1707 |   70609   179152 |   28524    1574    27094    17.2 | 12.052 % |
c |      1932 |   70609   179152 |   31376    1799    30446    16.9 | 12.053 % |
c |      2270 |   70196   178201 |   34514    2121    32259    15.2 | 12.597 % |
c ==============================================================================
c [1mFound solution: 2179[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2277 |   70204   178221 |   23401    2128    32301    15.2 | 12.597 % |
c |      2377 |   69756   177173 |   25741    2223    34819    15.7 | 13.223 % |
c |      2527 |   68491   174206 |   28315    2347    38087    16.2 | 14.893 % |
c ==============================================================================
c [1mFound solution: 2173[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2595 |   67333   171523 |   22444    2401    38686    16.1 | 14.893 % |
c |      2697 |   66571   169748 |   24688    2488    39496    15.9 | 17.501 % |
c ==============================================================================
c [1mFound solution: 2028[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2811 |   66573   169763 |   22191    2601    41964    16.1 | 17.501 % |
c |      2912 |   66338   169218 |   24410    2687    43291    16.1 | 18.031 % |
c ==============================================================================
c [1mFound solution: 1924[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2988 |   65410   167073 |   21803    2746    43707    15.9 | 18.031 % |
c |      3089 |   63386   162376 |   23983    2799    47959    17.1 | 21.953 % |
c |      3239 |   63386   162376 |   26381    2949    62040    21.0 | 21.953 % |
c |      3464 |   63386   162376 |   29019    3174    74050    23.3 | 21.953 % |
c |      3803 |   61775   158616 |   31921    3446    76816    22.3 | 24.199 % |
c |      4309 |   61422   157788 |   35113    3935   116814    29.7 | 24.657 % |
c ==============================================================================
c [1mFound solution: 1921[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4647 |   61453   157868 |   20484    4273   137525    32.2 | 24.657 % |
c |      4750 |   61453   157868 |   22532    4376   140697    32.2 | 24.650 % |
c |      4901 |   61453   157868 |   24785    4527   145200    32.1 | 24.650 % |
c |      5127 |   61453   157868 |   27264    4753   151738    31.9 | 24.650 % |
c |      5465 |   61349   157629 |   29990    5053   154257    30.5 | 24.780 % |
c |      5971 |   61349   157629 |   32989    5559   167280    30.1 | 24.780 % |
c ==============================================================================
c [1mFound solution: 1907[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6178 |   61445   157865 |   20481    5766   175207    30.4 | 24.780 % |
c |      6278 |   61232   157240 |   22529    5852   177409    30.3 | 24.977 % |
c ==============================================================================
c [1mFound solution: 1891[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6404 |   61201   157162 |   20400    5976   181572    30.4 | 24.977 % |
c |      6506 |   61194   157141 |   22440    6076   186499    30.7 | 25.023 % |
c |      6656 |   61174   157085 |   24684    6223   189898    30.5 | 25.040 % |
c |      6881 |   60935   156508 |   27152    6427   193656    30.1 | 25.385 % |
c |      7220 |   60725   156017 |   29867    6650   200513    30.2 | 25.635 % |
c ==============================================================================
c [1mFound solution: 1889[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7349 |   60733   156037 |   20244    6779   203446    30.0 | 25.635 % |
c |      7450 |   60733   156037 |   22268    6880   205758    29.9 | 25.635 % |
c |      7601 |   60728   156022 |   24495    7030   208603    29.7 | 25.640 % |
c |      7827 |   60728   156022 |   26944    7256   213972    29.5 | 25.640 % |
c |      8165 |   60551   155604 |   29639    7565   221473    29.3 | 25.877 % |
c |      8671 |   60156   154619 |   32603    8053   252963    31.4 | 26.338 % |
c |      9430 |   60004   154263 |   35863    8790   286402    32.6 | 26.540 % |
c |     10571 |   59190   152376 |   39449    9881   315307    31.9 | 27.643 % |
c |     12280 |   59107   152160 |   43394   11583   357293    30.8 | 27.729 % |
c ==============================================================================
c [1mFound solution: 1882[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12915 |   58997   151868 |   19665   12200   370350    30.4 | 27.729 % |
c |     13015 |   58997   151868 |   21631   12300   372395    30.3 | 27.856 % |
c |     13167 |   58958   151778 |   23794   12440   374194    30.1 | 27.912 % |
c |     13392 |   58831   151484 |   26174   12656   375759    29.7 | 28.076 % |
c ==============================================================================
c [1mFound solution: 1879[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13486 |   58087   149754 |   19362   12598   375795    29.8 | 28.076 % |
c |     13588 |   58087   149754 |   21298   12700   377802    29.7 | 29.115 % |
c |     13741 |   58087   149754 |   23428   12853   387259    30.1 | 29.115 % |
c |     13966 |   58087   149754 |   25770   13078   393630    30.1 | 29.115 % |
c |     14306 |   58087   149754 |   28347   13418   400516    29.8 | 29.115 % |
c |     14812 |   58087   149754 |   31182   13924   439892    31.6 | 29.115 % |
c |     15571 |   57870   149241 |   34300   14673   454378    31.0 | 29.399 % |
c |     16710 |   57870   149241 |   37731   15812   474459    30.0 | 29.399 % |
c |     18418 |   57134   147529 |   41504   17423   574127    33.0 | 30.441 % |
c |     20981 |   57134   147529 |   45654   19986   723332    36.2 | 30.441 % |
c ==============================================================================
c [1mFound solution: 1857[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21095 |   57151   147572 |   19050   20100   728049    36.2 | 30.441 % |
c |     21195 |   57130   147525 |   20955   20195   730320    36.2 | 30.465 % |
c |     21346 |   57130   147525 |   23050   20346   734030    36.1 | 30.465 % |
c ==============================================================================
c [1mFound solution: 1851[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21570 |   57125   147513 |   19041   20563   743827    36.2 | 30.465 % |
c ==============================================================================
c [1mFound solution: 1847[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21634 |   57128   147520 |   19042   20627   745630    36.1 | 30.465 % |
c |     21737 |   57128   147520 |   20946   20730   751945    36.3 | 30.471 % |
c |     21888 |   57045   147328 |   23040   20877   755676    36.2 | 30.574 % |
c |     22114 |   57045   147328 |   25344   21103   766990    36.3 | 30.574 % |
c |     22453 |   57020   147272 |   27879   21438   786878    36.7 | 30.604 % |
c |     22959 |   57020   147272 |   30667   21944   826660    37.7 | 30.604 % |
c ==============================================================================
c [1mFound solution: 1845[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23563 |   56971   147158 |   18990   22547   891231    39.5 | 30.604 % |
c |     23666 |   56971   147158 |   20889   22650   893152    39.4 | 30.675 % |
c |     23817 |   56971   147158 |   22977   22801   895145    39.3 | 30.675 % |
c |     24042 |   56971   147158 |   25275   23026   906809    39.4 | 30.675 % |
c |     24379 |   56971   147158 |   27803   23363   937813    40.1 | 30.675 % |
c |     24887 |   56669   146466 |   30583   23864   973509    40.8 | 31.071 % |
c ==============================================================================
c [1mFound solution: 1827[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25018 |   56676   146483 |   18892   23995   978086    40.8 | 31.071 % |
c |     25118 |   56676   146483 |   20781   24095   981131    40.7 | 31.071 % |
c |     25269 |   56676   146483 |   22859   24246   989880    40.8 | 31.071 % |
c |     25495 |   56676   146483 |   25145   24472  1001050    40.9 | 31.071 % |
c |     25832 |   56313   145647 |   27659   24774  1023643    41.3 | 31.575 % |
c ==============================================================================
c [1mFound solution: 1819[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25914 |   56316   145654 |   18772   24856  1031106    41.5 | 31.575 % |
c |     26016 |   56316   145654 |   20649   24958  1032870    41.4 | 31.576 % |
c |     26169 |   56316   145654 |   22714   25111  1046447    41.7 | 31.576 % |
c |     26394 |   56316   145654 |   24985   25336  1064844    42.0 | 31.576 % |
c |     26731 |   56292   145598 |   27484   25672  1075820    41.9 | 31.602 % |
c |     27238 |   56233   145459 |   30232   26178  1098939    42.0 | 31.680 % |
c |     27999 |   56159   145237 |   33255   26934  1182332    43.9 | 31.736 % |
c |     29141 |   56159   145237 |   36581   28076  1252716    44.6 | 31.736 % |
c |     30849 |   56150   145214 |   40239   29782  1351975    45.4 | 31.744 % |
c ==============================================================================
c [1mFound solution: 1789[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33214 |   56187   145307 |   18729   32147  1526468    47.5 | 31.744 % |
c |     33314 |   56187   145307 |   20601   16174   791453    48.9 | 31.735 % |
c |     33465 |   56187   145307 |   22662   16325   795339    48.7 | 31.735 % |
c |     33690 |   56187   145307 |   24928   16550   811934    49.1 | 31.735 % |
c |     34027 |   56187   145307 |   27421   16887   823519    48.8 | 31.735 % |
c ==============================================================================
c [1mFound solution: 1779[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34130 |   56203   145347 |   18734   16990   827111    48.7 | 31.735 % |
c |     34232 |   56203   145347 |   20607   17092   838120    49.0 | 31.733 % |
c |     34383 |   56203   145347 |   22668   17243   842134    48.8 | 31.733 % |
c ==============================================================================
c [1mFound solution: 1778[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34597 |   56213   145371 |   18737   17457   872147    50.0 | 31.733 % |
c |     34697 |   56205   145353 |   20610   17555   873761    49.8 | 31.740 % |
c |     34847 |   56163   145256 |   22671   17697   875346    49.5 | 31.796 % |
c |     35074 |   55614   143980 |   24938   17713   880296    49.7 | 32.527 % |
c |     35411 |   55614   143980 |   27432   18050   891405    49.4 | 32.527 % |
c |     35920 |   55614   143980 |   30176   18559   929733    50.1 | 32.527 % |
c |     36681 |   55614   143980 |   33193   19320   983705    50.9 | 32.527 % |
c |     37820 |   55614   143980 |   36513   20459  1065761    52.1 | 32.527 % |
c ==============================================================================
c [1mFound solution: 1771[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39153 |   55618   143990 |   18539   21792  1168350    53.6 | 32.527 % |
c |     39254 |   55618   143990 |   20392   21893  1171941    53.5 | 32.528 % |
c |     39409 |   55618   143990 |   22432   22048  1182758    53.6 | 32.528 % |
c |     39634 |   55618   143990 |   24675   22273  1190256    53.4 | 32.528 % |
c |     39971 |   55618   143990 |   27142   22610  1198970    53.0 | 32.528 % |
c |     40478 |   55618   143990 |   29857   23117  1241336    53.7 | 32.528 % |
c |     41238 |   55443   143587 |   32842   23871  1300327    54.5 | 32.760 % |
c |     42377 |   55436   143566 |   36127   25007  1332385    53.3 | 32.765 % |
c |     44085 |   55436   143566 |   39739   26715  1385367    51.9 | 32.765 % |
c |     46647 |   55427   143543 |   43713   29276  1512944    51.7 | 32.773 % |
c ==============================================================================
c [1mFound solution: 1761[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48332 |   55435   143563 |   18478   30961  1620159    52.3 | 32.773 % |
c |     48432 |   55435   143563 |   20325   15581   569217    36.5 | 32.773 % |
c |     48583 |   55435   143563 |   22358   15732   576354    36.6 | 32.773 % |
c |     48809 |   55435   143563 |   24594   15958   586916    36.8 | 32.773 % |
c ==============================================================================
c [1mFound solution: 1751[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49011 |   55440   143576 |   18480   16160   598362    37.0 | 32.773 % |
c |     49113 |   55440   143576 |   20328   16262   600587    36.9 | 32.775 % |
c |     49263 |   55440   143576 |   22360   16412   615724    37.5 | 32.775 % |
c |     49489 |   55433   143555 |   24596   16636   623173    37.5 | 32.779 % |
c |     49828 |   55433   143555 |   27056   16975   630918    37.2 | 32.779 % |
c |     50335 |   55433   143555 |   29762   17482   641582    36.7 | 32.779 % |
c |     51094 |   55424   143532 |   32738   18238   662543    36.3 | 32.788 % |
c |     52233 |   55290   143205 |   36012   19369   727221    37.5 | 32.951 % |
c |     53942 |   55283   143184 |   39613   21074   777289    36.9 | 32.955 % |
c ==============================================================================
c [1mFound solution: 1730[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55465 |   55305   143238 |   18435   22597   906318    40.1 | 32.955 % |
c |     55565 |   55073   142698 |   20278   22684   907310    40.0 | 33.250 % |
c |     55716 |   54831   142145 |   22306   22812   916789    40.2 | 33.556 % |
c |     55941 |   54831   142145 |   24536   23037   931838    40.4 | 33.555 % |
c |     56279 |   54686   141799 |   26990   23355   940703    40.3 | 33.749 % |
c |     56786 |   54679   141778 |   29689   23860   965722    40.5 | 33.753 % |
c |     57547 |   54679   141778 |   32658   24621   993342    40.3 | 33.753 % |
c |     58686 |   54584   141534 |   35924   25756  1053248    40.9 | 33.869 % |
c |     60394 |   54584   141534 |   39517   27464  1209356    44.0 | 33.869 % |
c |     62956 |   54579   141519 |   43468   30024  1362239    45.4 | 33.873 % |
c ==============================================================================
c [1mFound solution: 1709[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63218 |   54585   141533 |   18195   30286  1374583    45.4 | 33.873 % |
c |     63318 |   54585   141533 |   20014   15243   636385    41.7 | 33.873 % |
c |     63468 |   54585   141533 |   22015   15393   643684    41.8 | 33.873 % |
c |     63693 |   54585   141533 |   24217   15618   663543    42.5 | 33.873 % |
c |     64033 |   54585   141533 |   26639   15958   689700    43.2 | 33.873 % |
c |     64540 |   54569   141485 |   29303   16462   710848    43.2 | 33.886 % |
c |     65299 |   54556   141448 |   32233   17219   746818    43.4 | 33.899 % |
c |     66438 |   54556   141448 |   35456   18358   860808    46.9 | 33.899 % |
c |     68149 |   54556   141448 |   39002   20069   969043    48.3 | 33.899 % |
c ==============================================================================
c [1mFound solution: 1708[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69591 |   54563   141465 |   18187   21511  1057309    49.2 | 33.899 % |
c |     69692 |   54483   141280 |   20005   21601  1058935    49.0 | 34.011 % |
c |     69842 |   54483   141280 |   22006   21751  1067573    49.1 | 34.010 % |
c |     70069 |   54483   141280 |   24206   21978  1078942    49.1 | 34.010 % |
c |     70407 |   54483   141280 |   26627   22316  1102923    49.4 | 34.010 % |
c |     70914 |   54474   141257 |   29290   22820  1129045    49.5 | 34.019 % |
c |     71677 |   54192   140581 |   32219   23569  1181684    50.1 | 34.380 % |
c |     72817 |   54170   140523 |   35441   24706  1248961    50.6 | 34.401 % |
c ==============================================================================
c [1mFound solution: 1704[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73953 |   54176   140537 |   18058   25842  1331297    51.5 | 34.401 % |
c |     74054 |   54176   140537 |   19863   25943  1334005    51.4 | 34.401 % |
c |     74205 |   54168   140515 |   21850   26093  1343025    51.5 | 34.410 % |
c |     74431 |   54168   140515 |   24035   26319  1348240    51.2 | 34.410 % |
c |     74769 |   54168   140515 |   26438   26657  1359724    51.0 | 34.410 % |
c |     75275 |   53782   139616 |   29082   27138  1367750    50.4 | 34.929 % |
c |     76034 |   53666   139350 |   31990   27883  1422181    51.0 | 35.080 % |
c |     77175 |   53666   139350 |   35189   29024  1499346    51.7 | 35.080 % |
c |     78883 |   53661   139335 |   38708   30729  1570989    51.1 | 35.084 % |
c ==============================================================================
c [1mFound solution: 1701[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79115 |   53667   139349 |   17889   30961  1595829    51.5 | 35.084 % |
c |     79216 |   53667   139349 |   19677   15582   557033    35.7 | 35.084 % |
c |     79372 |   53667   139349 |   21645   15738   564117    35.8 | 35.084 % |
c |     79597 |   53667   139349 |   23810   15963   575906    36.1 | 35.084 % |
c |     79934 |   53667   139349 |   26191   16300   596618    36.6 | 35.084 % |
c |     80440 |   53667   139349 |   28810   16806   637980    38.0 | 35.084 % |
c ==============================================================================
c [1mFound solution: 1681[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80786 |   53694   139418 |   17898   17152   669439    39.0 | 35.084 % |
c |     80886 |   53694   139418 |   19687   17252   674169    39.1 | 35.074 % |
c |     81036 |   53694   139418 |   21656   17402   682240    39.2 | 35.074 % |
c |     81261 |   53694   139418 |   23822   17627   692778    39.3 | 35.074 % |
c |     81598 |   53694   139418 |   26204   17964   707014    39.4 | 35.074 % |
c |     82105 |   53694   139418 |   28824   18471   734735    39.8 | 35.074 % |
c |     82864 |   53694   139418 |   31707   19230   761208    39.6 | 35.074 % |
c |     84004 |   53694   139418 |   34878   20370   807262    39.6 | 35.074 % |
c |     85713 |   53636   139247 |   38365   22064   869533    39.4 | 35.122 % |
c |     88275 |   53636   139247 |   42202   24626  1028052    41.7 | 35.122 % |
c |     92123 |   53636   139247 |   46422   28474  1285993    45.2 | 35.122 % |
c |     97889 |   53636   139247 |   51065   34240  1645858    48.1 | 35.122 % |
c ==============================================================================
c [1mFound solution: 1679[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    101348 |   53649   139280 |   17883   37699  1869282    49.6 | 35.122 % |
c |    101449 |   53649   139280 |   19671   17648   788473    44.7 | 35.120 % |
c |    101599 |   53649   139280 |   21638   17798   798338    44.9 | 35.120 % |
c |    101824 |   53464   138850 |   23802   18006   806059    44.8 | 35.373 % |
c |    102161 |   53464   138850 |   26182   18343   820610    44.7 | 35.373 % |
c |    102669 |   53464   138850 |   28800   18851   828169    43.9 | 35.373 % |
c |    103428 |   53433   138779 |   31680   19608   854709    43.6 | 35.416 % |
c |    104567 |   53433   138779 |   34848   20747   909381    43.8 | 35.416 % |
c |    106275 |   53433   138779 |   38333   22455   981995    43.7 | 35.416 % |
c |    108839 |   53409   138709 |   42167   25013  1091899    43.7 | 35.438 % |
c ==============================================================================
c [1mFound solution: 1675[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111459 |   53417   138729 |   17805   27633  1215412    44.0 | 35.438 % |
c |    111560 |   53417   138729 |   19585   13918   416627    29.9 | 35.437 % |
c |    111710 |   53417   138729 |   21544   14068   423829    30.1 | 35.437 % |
c |    111936 |   53417   138729 |   23698   14294   431416    30.2 | 35.437 % |
c |    112275 |   53417   138729 |   26068   14633   450898    30.8 | 35.437 % |
c |    112781 |   53417   138729 |   28675   15139   481538    31.8 | 35.437 % |
c |    113541 |   53417   138729 |   31542   15899   529961    33.3 | 35.437 % |
c |    114680 |   53417   138729 |   34696   17038   592837    34.8 | 35.437 % |
c |    116388 |   53291   138436 |   38166   18722   655572    35.0 | 35.617 % |
c |    118952 |   53142   138090 |   41983   21251   834890    39.3 | 35.819 % |
c |    122797 |   53142   138090 |   46181   25096  1015052    40.4 | 35.819 % |
c |    128563 |   53142   138090 |   50799   30862  1260163    40.8 | 35.819 % |
c |    137214 |   53132   138063 |   55879   39507  1747123    44.2 | 35.828 % |
c ==============================================================================
c [1mFound solution: 1674[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    144513 |   53076   137933 |   17692   46804  2162886    46.2 | 35.828 % |
c |    144614 |   53076   137933 |   19461   19538   755239    38.7 | 35.913 % |
c |    144765 |   53076   137933 |   21407   19689   759014    38.6 | 35.913 % |
c |    144990 |   53076   137933 |   23548   19914   771862    38.8 | 35.913 % |
c |    145329 |   53076   137933 |   25902   20253   790174    39.0 | 35.913 % |
c |    145837 |   53076   137933 |   28493   20761   816689    39.3 | 35.913 % |
c |    146597 |   53076   137933 |   31342   21521   854194    39.7 | 35.913 % |
c |    147736 |   53076   137933 |   34476   22660   909307    40.1 | 35.913 % |
c |    149444 |   53076   137933 |   37924   24368   977408    40.1 | 35.913 % |
c ==============================================================================
c [1mFound solution: 1673[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150144 |   53079   137938 |   17693   25067  1018697    40.6 | 35.913 % |
c |    150244 |   53079   137938 |   19462   25167  1023272    40.7 | 35.917 % |
c |    150394 |   53079   137938 |   21408   25317  1027428    40.6 | 35.917 % |
c |    150619 |   52948   137633 |   23549   25530  1035370    40.6 | 36.102 % |
c |    150956 |   52811   137306 |   25904   25842  1047899    40.6 | 36.269 % |
c |    151464 |   52811   137306 |   28494   26350  1070170    40.6 | 36.269 % |
c |    152224 |   52811   137306 |   31344   27110  1094861    40.4 | 36.269 % |
c |    153363 |   52811   137306 |   34478   28249  1140635    40.4 | 36.269 % |
c |    155071 |   52811   137306 |   37926   29957  1211321    40.4 | 36.269 % |
c |    157633 |   52742   137146 |   41719   32516  1353392    41.6 | 36.368 % |
c |    161477 |   52691   137025 |   45891   36347  1573604    43.3 | 36.432 % |
c ==============================================================================
c [1mFound solution: 1671[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165192 |   52695   137035 |   17565   40062  1768654    44.1 | 36.432 % |
c |    165292 |   52695   137035 |   19321   19125   689106    36.0 | 36.433 % |
c |    165442 |   52695   137035 |   21253   19275   695771    36.1 | 36.433 % |
c |    165670 |   52695   137035 |   23379   19503   711946    36.5 | 36.433 % |
c |    166008 |   52695   137035 |   25716   19841   725279    36.6 | 36.433 % |
c |    166514 |   52695   137035 |   28288   20347   746787    36.7 | 36.433 % |
c ==============================================================================
c [1mFound solution: 1668[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    166994 |   52699   137045 |   17566   20827   770393    37.0 | 36.433 % |
c |    167095 |   52699   137045 |   19322   20928   777479    37.2 | 36.434 % |
c |    167247 |   52699   137045 |   21254   21080   791718    37.6 | 36.434 % |
c |    167474 |   52699   137045 |   23380   21307   799949    37.5 | 36.434 % |
c |    167811 |   52699   137045 |   25718   21644   815385    37.7 | 36.434 % |
c |    168317 |   52699   137045 |   28290   22150   847982    38.3 | 36.434 % |
c |    169078 |   52699   137045 |   31119   22911   877800    38.3 | 36.434 % |
c |    170218 |   52699   137045 |   34231   24051   927360    38.6 | 36.434 % |
c |    171926 |   52699   137045 |   37654   25759  1026430    39.8 | 36.434 % |
c |    174491 |   52699   137045 |   41419   28324  1168146    41.2 | 36.434 % |
c ==============================================================================
c [1mFound solution: 1659[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175110 |   52703   137055 |   17567   28943  1215179    42.0 | 36.434 % |
c |    175212 |   52652   136935 |   19323   14572   480982    33.0 | 36.517 % |
c |    175362 |   52652   136935 |   21256   14722   490944    33.3 | 36.517 % |
c |    175588 |   52649   136929 |   23381   14946   505311    33.8 | 36.521 % |
c |    175928 |   52649   136929 |   25719   15286   524060    34.3 | 36.521 % |
c |    176435 |   52649   136929 |   28291   15793   549075    34.8 | 36.521 % |
c |    177194 |   52649   136929 |   31121   16552   587540    35.5 | 36.521 % |
c |    178334 |   52649   136929 |   34233   17692   646778    36.6 | 36.521 % |
c ==============================================================================
c [1mFound solution: 1651[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    179859 |   52653   136939 |   17551   19217   741511    38.6 | 36.521 % |
c |    179959 |   52653   136939 |   19306   19317   746063    38.6 | 36.522 % |
c |    180109 |   52653   136939 |   21236   19467   753313    38.7 | 36.522 % |
c |    180334 |   52653   136939 |   23360   19692   762998    38.7 | 36.522 % |
c |    180672 |   52653   136939 |   25696   20030   780628    39.0 | 36.522 % |
c |    181179 |   52653   136939 |   28266   20537   810883    39.5 | 36.522 % |
c |    181938 |   52653   136939 |   31092   21296   849267    39.9 | 36.522 % |
c |    183077 |   52653   136939 |   34201   22435   899688    40.1 | 36.522 % |
c |    184786 |   52643   136916 |   37622   24139   992629    41.1 | 36.535 % |
c |    187348 |   52639   136906 |   41384   26700  1120688    42.0 | 36.539 % |
c ==============================================================================
c [1mFound solution: 1648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188862 |   52646   136923 |   17548   28214  1228249    43.5 | 36.539 % |
c |    188962 |   52646   136923 |   19302   14207   469546    33.1 | 36.539 % |
c |    189112 |   52646   136923 |   21233   14357   474223    33.0 | 36.539 % |
c |    189339 |   52646   136923 |   23356   14584   483674    33.2 | 36.539 % |
c |    189676 |   52646   136923 |   25692   14921   500108    33.5 | 36.539 % |
c |    190182 |   52646   136923 |   28261   15427   522460    33.9 | 36.539 % |
c |    190943 |   52646   136923 |   31087   16188   557553    34.4 | 36.539 % |
c |    192082 |   52646   136923 |   34196   17327   599942    34.6 | 36.539 % |
c |    193792 |   52646   136923 |   37615   19037   717191    37.7 | 36.539 % |
c |    196354 |   52632   136885 |   41377   21594   806921    37.4 | 36.552 % |
c |    200198 |   52080   135597 |   45514   25416  1020646    40.2 | 37.324 % |
c |    205964 |   52080   135597 |   50066   31182  1315835    42.2 | 37.324 % |
c |    214613 |   52067   135564 |   55073   39828  1789558    44.9 | 37.337 % |
c |    227587 |   52067   135564 |   60580   52802  2635487    49.9 | 37.337 % |
c ==============================================================================
c [1mFound solution: 1639[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    239337 |   52047   135506 |   17349   64547  3435785    53.2 | 37.337 % |
c |    239438 |   52047   135506 |   19083   21363   926240    43.4 | 37.359 % |
c |    239590 |   52047   135506 |   20992   21515   932551    43.3 | 37.359 % |
c |    239815 |   52047   135506 |   23091   21740   941576    43.3 | 37.359 % |
c |    240154 |   52047   135506 |   25400   22079   952174    43.1 | 37.359 % |
c |    240661 |   52047   135506 |   27940   22586   977468    43.3 | 37.359 % |
c |    241421 |   52047   135506 |   30734   23346  1027014    44.0 | 37.359 % |
c |    242565 |   52047   135506 |   33808   24490  1076721    44.0 | 37.359 % |
#### 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.78 0.95 0.94 2/54 22181
Raw data (stat): 22181 (runsolver) R 22180 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491747314 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.81 0.95 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2436 0 0 0 991 7 0 0 25 0 1 0 491747314 12017664 2362 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2934 2362 603 41 0 2893 0
vsize: 11736
[startup+19.9997 s]
Raw data (loadavg): 0.84 0.95 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2539 0 0 0 1991 7 0 0 25 0 1 0 491747314 12447744 2465 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3039 2465 603 41 0 2998 0
vsize: 12156
[startup+30.0008 s]
Raw data (loadavg): 0.86 0.95 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2622 0 0 0 2990 7 0 0 25 0 1 0 491747314 12877824 2548 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3144 2548 603 41 0 3103 0
vsize: 12576
[startup+40.0004 s]
Raw data (loadavg): 0.89 0.95 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2734 0 0 0 3990 7 0 0 25 0 1 0 491747314 13312000 2660 4294967295 134512640 134672761 3221224544 3221223728 134559313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3250 2660 603 41 0 3209 0
vsize: 13000
[startup+50.0012 s]
Raw data (loadavg): 0.90 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2831 0 0 0 4990 8 0 0 25 0 1 0 491747314 13647872 2757 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3332 2757 603 41 0 3291 0
vsize: 13328
[startup+60.0016 s]
Raw data (loadavg): 0.92 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2923 0 0 0 5990 8 0 0 25 0 1 0 491747314 14049280 2849 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3430 2849 603 41 0 3389 0
vsize: 13720
[startup+70.0018 s]
Raw data (loadavg): 0.93 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3063 0 0 0 6989 8 0 0 25 0 1 0 491747314 14729216 2989 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3596 2989 603 41 0 3555 0
vsize: 14384
[startup+80.0027 s]
Raw data (loadavg): 0.94 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3236 0 0 0 7988 10 0 0 25 0 1 0 491747314 15392768 3162 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3758 3162 603 41 0 3717 0
vsize: 15032
[startup+90.0028 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3407 0 0 0 8988 10 0 0 25 0 1 0 491747314 16027648 3333 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3913 3333 603 41 0 3872 0
vsize: 15652
[startup+100.003 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3558 0 0 0 9988 10 0 0 25 0 1 0 491747314 16687104 3484 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4074 3484 603 41 0 4033 0
vsize: 16296
[startup+110.004 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3717 0 0 0 10987 11 0 0 25 0 1 0 491747314 17350656 3643 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4236 3643 603 41 0 4195 0
vsize: 16944
[startup+120.004 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3845 0 0 0 11987 11 0 0 25 0 1 0 491747314 17879040 3771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4365 3771 603 41 0 4324 0
vsize: 17460
[startup+130.005 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3968 0 0 0 12987 12 0 0 25 0 1 0 491747314 18407424 3894 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4494 3894 603 41 0 4453 0
vsize: 17976
[startup+140.005 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 22181
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4124 0 0 0 13986 12 0 0 25 0 1 0 491747314 18939904 4050 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4624 4050 603 41 0 4583 0
vsize: 18496
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 14986 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+160.006 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 15986 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+170.006 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 16987 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 17987 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 18987 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 19987 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4656 4084 603 41 0 4615 0
vsize: 18624
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4266 0 0 0 20987 14 0 0 25 0 1 0 491747314 19595264 4192 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4784 4192 603 41 0 4743 0
vsize: 19136
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 21986 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 22987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 23987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 24987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134559922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 25987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 26987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 27988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 28988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 29988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 30988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+320.009 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 31988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+330.011 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 32988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+340.01 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 33988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+350.011 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 34989 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4247 603 41 0 4782 0
vsize: 19292
[startup+360.012 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 35989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+370.012 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 36989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+380.011 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 37989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+390.012 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 38989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+400.012 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 39989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+410.012 s]
Raw data (loadavg): 1.17 1.02 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 40989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+420.012 s]
Raw data (loadavg): 1.14 1.02 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 41990 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+430.013 s]
Raw data (loadavg): 1.12 1.02 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 42990 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+440.012 s]
Raw data (loadavg): 1.10 1.02 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 43990 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4322 603 41 0 4857 0
vsize: 19592
[startup+450.014 s]
Raw data (loadavg): 1.08 1.02 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4491 0 0 0 44990 15 0 0 25 0 1 0 491747314 20586496 4417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5026 4417 603 41 0 4985 0
vsize: 20104
[startup+460.013 s]
Raw data (loadavg): 1.07 1.02 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4625 0 0 0 45990 15 0 0 25 0 1 0 491747314 21118976 4551 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5156 4551 603 41 0 5115 0
vsize: 20624
[startup+470.014 s]
Raw data (loadavg): 1.06 1.01 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 46990 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+480.014 s]
Raw data (loadavg): 1.05 1.01 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 47990 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+490.014 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 48990 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+500.014 s]
Raw data (loadavg): 1.12 1.03 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 49990 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+510.014 s]
Raw data (loadavg): 1.17 1.04 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 50991 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4679 603 41 0 5241 0
vsize: 21128
[startup+520.015 s]
Raw data (loadavg): 1.14 1.04 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 51991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+530.015 s]
Raw data (loadavg): 1.12 1.04 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 52991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+540.015 s]
Raw data (loadavg): 1.10 1.04 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 53991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+550.016 s]
Raw data (loadavg): 1.09 1.04 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 54991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+560.015 s]
Raw data (loadavg): 1.07 1.03 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 55991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+570.015 s]
Raw data (loadavg): 1.06 1.03 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 56992 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+580.017 s]
Raw data (loadavg): 1.05 1.03 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 57992 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+590.017 s]
Raw data (loadavg): 1.04 1.03 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 58992 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+600.018 s]
Raw data (loadavg): 1.04 1.03 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 59992 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+610.019 s]
Raw data (loadavg): 1.03 1.03 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 60993 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+620.018 s]
Raw data (loadavg): 1.02 1.03 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 61993 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+630.018 s]
Raw data (loadavg): 1.02 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 62993 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4679 603 41 0 5240 0
vsize: 21124
[startup+640.02 s]
Raw data (loadavg): 1.02 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4755 0 0 0 63993 15 0 0 25 0 1 0 491747314 21630976 4681 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5281 4681 603 41 0 5240 0
vsize: 21124
[startup+650.02 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4791 0 0 0 64993 15 0 0 25 0 1 0 491747314 21766144 4717 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5314 4717 603 41 0 5273 0
vsize: 21256
[startup+660.02 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4874 0 0 0 65993 15 0 0 25 0 1 0 491747314 22167552 4800 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5412 4800 603 41 0 5371 0
vsize: 21648
[startup+670.02 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4993 0 0 0 66993 16 0 0 25 0 1 0 491747314 22691840 4919 4294967295 134512640 134672761 3221224544 3221223728 134559351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5540 4919 603 41 0 5499 0
vsize: 22160
[startup+680.02 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5114 0 0 0 67993 16 0 0 25 0 1 0 491747314 23085056 5040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5636 5040 603 41 0 5595 0
vsize: 22544
[startup+690.02 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 68993 16 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+700.021 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 69993 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+710.022 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 70993 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+720.022 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 71993 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+730.023 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 72993 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+740.023 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 73994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+750.024 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 74994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+760.025 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 75994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+770.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 76994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+780.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 77994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5719 5122 603 41 0 5678 0
vsize: 22876
[startup+790.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 78994 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+800.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 79995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+810.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 80995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+820.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 81995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+830.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 82995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+840.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 83995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+850.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 84995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+860.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 85996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+870.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 86996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+880.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 87996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223628 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+890.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 88996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+900.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 89996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+910.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 90997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+920.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 91997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+930.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 92997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+940.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 93997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+950.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 94997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+960.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 95998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+970.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 96998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+980.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 97998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+990.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 98998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 99998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 100999 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 101999 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 102999 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 103999 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 105000 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5138 603 41 0 5702 0
vsize: 22972
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5279 0 0 0 105999 17 0 0 25 0 1 0 491747314 23785472 5205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5807 5205 603 41 0 5766 0
vsize: 23228
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5403 0 0 0 106999 18 0 0 25 0 1 0 491747314 24313856 5329 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5936 5329 603 41 0 5895 0
vsize: 23744
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5514 0 0 0 107999 18 0 0 25 0 1 0 491747314 24752128 5440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6043 5440 603 41 0 6002 0
vsize: 24172
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5625 0 0 0 108998 19 0 0 25 0 1 0 491747314 25276416 5551 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6171 5551 603 41 0 6130 0
vsize: 24684
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5739 0 0 0 109998 19 0 0 25 0 1 0 491747314 25669632 5665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6267 5665 603 41 0 6226 0
vsize: 25068
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5881 0 0 0 110999 19 0 0 25 0 1 0 491747314 26365952 5807 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6437 5807 603 41 0 6396 0
vsize: 25748
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5996 0 0 0 111998 20 0 0 25 0 1 0 491747314 26763264 5922 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6534 5922 603 41 0 6493 0
vsize: 26136
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6108 0 0 0 112999 20 0 0 25 0 1 0 491747314 27299840 6034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6665 6034 603 41 0 6624 0
vsize: 26660
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6233 0 0 0 113998 20 0 0 25 0 1 0 491747314 27697152 6159 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6762 6159 603 41 0 6721 0
vsize: 27048
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6355 0 0 0 114998 21 0 0 25 0 1 0 491747314 28233728 6281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6893 6281 603 41 0 6852 0
vsize: 27572
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6494 0 0 0 115998 21 0 0 25 0 1 0 491747314 28774400 6420 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7025 6420 603 41 0 6984 0
vsize: 28100
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6611 0 0 0 116998 21 0 0 25 0 1 0 491747314 29306880 6537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7155 6537 603 41 0 7114 0
vsize: 28620
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6718 0 0 0 117997 22 0 0 25 0 1 0 491747314 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6718 0 0 0 118998 22 0 0 25 0 1 0 491747314 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 22183
Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6718 0 0 0 119998 22 0 0 25 0 1 0 491747314 29679616 6644 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7246 6644 603 41 0 7205 0
vsize: 28984
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 22183
Raw data (stat): 22181 (minisat+) Z 22180 29151 29150 0 -1 12 6721 0 0 0 119998 23 0 0 25 0 1 0 491747314 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.22
CPU user time (s): 1199.99
CPU system time (s): 0.236963
CPU usage (%): 100.013
Max. virtual memory (Kb): 28984
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####