Some explanations

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

General information on the benchmark

Namemps-v2-20-10/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-20-10-maros.opb
MD5SUMdf23206734a7a5ecc1a5d03632e7fa81
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 344750
Optimality of the best value was proved YES
Number of terms in the objective function 90
Biggest coefficient in the objective function 4831838208
Number of bits for the biggest coefficient in the objective function 33
Sum of the numbers in the objective function 15032909794
Number of bits of the sum of numbers in the objective function 34
Biggest number in a constraint 4831838208
Number of bits of the biggest number in a constraint 33
Biggest sum of numbers in a constraint 15032909794
Number of bits of the biggest sum of numbers34
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark30.9553
Number of variables90
Total number of constraints6
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints6
Minimum length of a constraint15
Maximum length of a constraint90

Trace number 5927

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-20 02:26:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3127 boxname=wulflinc21 idbench=783 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  df23206734a7a5ecc1a5d03632e7fa81  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-maros.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-maros.opb
IDLAUNCH: 3127
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        840356 kB
Buffers:         30952 kB
Cached:         133636 kB
SwapCached:        788 kB
Active:          50088 kB
Inactive:       117004 kB
HighTotal:      131008 kB
HighFree:        24108 kB
LowTotal:       903652 kB
LowFree:        816248 kB
SwapTotal:     2097892 kB
SwapFree:      2096456 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            21572 kB
Committed_AS:    64368 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:27:21 (client local time) WITH STATUS 30 IN 30.9553 SECONDS
stats: 3127 0 30.9553 30

Solver Data

c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): s
c ---[   5]---> BDD-cost:   14
c ---[   3]---> Sorter-cost: 1222     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  546     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5697    13365 |    1899       0        0     nan |  0.000 % |
c |       102 |    5697    13365 |    2088     102     2002    19.6 |  1.781 % |
c ==============================================================================
c Found solution: 423991
c ---[   0]---> Sorter-cost: 1242     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       151 |    8635    20227 |    2878     151     2317    15.3 |  1.781 % |
c ==============================================================================
c Found solution: 420608
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       167 |    8677    20361 |    2892     167     2472    14.8 |  1.781 % |
c ==============================================================================
c Found solution: 391113
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       198 |    8689    20396 |    2896     198     2965    15.0 |  1.781 % |
c |       298 |    8689    20396 |    3185     298     3751    12.6 |  1.263 % |
c ==============================================================================
c Found solution: 384569
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       308 |    8706    20438 |    2902     308     3907    12.7 |  1.263 % |
c |       408 |    8706    20438 |    3192     408     5000    12.3 |  1.290 % |
c |       559 |    8706    20438 |    3511     559     7666    13.7 |  1.290 % |
c ==============================================================================
c Found solution: 383973
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       710 |    8723    20477 |    2907     710     9537    13.4 |  1.290 % |
c |       810 |    8723    20477 |    3197     810    10487    12.9 |  1.319 % |
c ==============================================================================
c Found solution: 370341
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       922 |    8741    20519 |    2913     922    12814    13.9 |  1.319 % |
c |      1023 |    8741    20519 |    3204    1023    14426    14.1 |  1.347 % |
c ==============================================================================
c Found solution: 359039
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1069 |    8758    20565 |    2919    1069    14863    13.9 |  1.347 % |
c |      1169 |    8758    20565 |    3210    1169    16648    14.2 |  1.374 % |
c |      1319 |    8758    20565 |    3531    1319    18753    14.2 |  1.374 % |
c |      1544 |    8758    20565 |    3885    1544    21347    13.8 |  1.374 % |
c |      1882 |    8758    20565 |    4273    1882    25220    13.4 |  1.374 % |
c |      2391 |    8758    20565 |    4701    2391    32011    13.4 |  1.374 % |
c ==============================================================================
c Found solution: 352165
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2781 |    8765    20587 |    2921    2781    39871    14.3 |  1.374 % |
c |      2882 |    8765    20587 |    3213    2882    41280    14.3 |  1.403 % |
c |      3035 |    8765    20587 |    3534    3035    43433    14.3 |  1.403 % |
c |      3261 |    8765    20587 |    3887    3261    48979    15.0 |  1.403 % |
c |      3598 |    8765    20587 |    4276    3598    54378    15.1 |  1.403 % |
c |      4106 |    8765    20587 |    4704    4106    64249    15.6 |  1.403 % |
c ==============================================================================
c Found solution: 351712
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4333 |    8775    20617 |    2925    4333    67578    15.6 |  1.403 % |
c |      4434 |    8775    20617 |    3217    2268    34255    15.1 |  1.431 % |
c |      4585 |    8775    20617 |    3539    2419    36143    14.9 |  1.431 % |
c |      4810 |    8775    20617 |    3893    2644    38975    14.7 |  1.431 % |
c ==============================================================================
c Found solution: 351204
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5031 |    8791    20655 |    2930    2865    43803    15.3 |  1.431 % |
c |      5131 |    8791    20655 |    3223    2965    45101    15.2 |  1.459 % |
c |      5282 |    8791    20655 |    3545    3116    46766    15.0 |  1.459 % |
c ==============================================================================
c Found solution: 351203
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5491 |    8798    20674 |    2932    3325    49903    15.0 |  1.459 % |
c |      5594 |    8798    20674 |    3225    1766    21211    12.0 |  1.488 % |
c |      5746 |    8798    20674 |    3547    1918    23871    12.4 |  1.488 % |
c |      5972 |    8798    20674 |    3902    2144    27610    12.9 |  1.488 % |
c |      6309 |    8798    20674 |    4292    2481    33375    13.5 |  1.488 % |
c ==============================================================================
c Found solution: 350714
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6448 |    8819    20725 |    2939    2620    35479    13.5 |  1.488 % |
c |      6550 |    8819    20725 |    3232    2722    37924    13.9 |  1.513 % |
c |      6700 |    8819    20725 |    3556    2872    40741    14.2 |  1.513 % |
c |      6925 |    8819    20725 |    3911    3097    44519    14.4 |  1.513 % |
c |      7262 |    8819    20725 |    4302    3434    50652    14.8 |  1.513 % |
c ==============================================================================
c Found solution: 350066
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7445 |    8834    20764 |    2944    3617    53698    14.8 |  1.513 % |
c |      7546 |    8834    20764 |    3238    1910    23165    12.1 |  1.540 % |
c |      7700 |    8834    20764 |    3562    2064    24536    11.9 |  1.540 % |
c |      7925 |    8834    20764 |    3918    2289    29408    12.8 |  1.540 % |
c |      8262 |    8834    20764 |    4310    2626    35596    13.6 |  1.540 % |
c |      8768 |    8834    20764 |    4741    3132    44465    14.2 |  1.540 % |
c |      9527 |    8834    20764 |    5215    3891    56817    14.6 |  1.540 % |
c ==============================================================================
c Found solution: 348198
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9708 |    8854    20810 |    2951    4072    60279    14.8 |  1.540 % |
c |      9808 |    8854    20810 |    3246    2136    24643    11.5 |  1.566 % |
c |      9961 |    8854    20810 |    3570    2289    26558    11.6 |  1.567 % |
c |     10186 |    8854    20810 |    3927    2514    31320    12.5 |  1.567 % |
c |     10525 |    8854    20810 |    4320    2853    37361    13.1 |  1.567 % |
c |     11031 |    8854    20810 |    4752    3359    45443    13.5 |  1.566 % |
c ==============================================================================
c Found solution: 348151
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11515 |    8868    20842 |    2956    3843    54113    14.1 |  1.566 % |
c |     11617 |    8868    20842 |    3251    2024    22531    11.1 |  1.594 % |
c |     11767 |    8868    20842 |    3576    2174    24167    11.1 |  1.594 % |
c |     11993 |    8868    20842 |    3934    2400    26755    11.1 |  1.594 % |
c |     12330 |    8868    20842 |    4327    2737    31077    11.4 |  1.595 % |
c |     12836 |    8868    20842 |    4760    3243    42263    13.0 |  1.594 % |
c ==============================================================================
c Found solution: 348139
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13046 |    8884    20878 |    2961    3453    45788    13.3 |  1.594 % |
c |     13148 |    8884    20878 |    3257    1829    21584    11.8 |  1.622 % |
c |     13298 |    8884    20878 |    3582    1979    23723    12.0 |  1.622 % |
c ==============================================================================
c Found solution: 348133
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13351 |    8894    20902 |    2964    2032    24568    12.1 |  1.622 % |
c |     13451 |    8894    20902 |    3260    2132    26507    12.4 |  1.650 % |
c |     13602 |    8894    20902 |    3586    2283    29085    12.7 |  1.650 % |
c |     13827 |    8894    20902 |    3945    2508    34003    13.6 |  1.649 % |
c ==============================================================================
c Found solution: 348128
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13899 |    8902    20924 |    2967    2580    35575    13.8 |  1.649 % |
c ==============================================================================
c Found solution: 348117
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13988 |    8913    20957 |    2971    2669    37250    14.0 |  1.649 % |
c |     14088 |    8913    20957 |    3268    2769    39246    14.2 |  1.705 % |
c |     14238 |    8913    20957 |    3594    2919    41757    14.3 |  1.705 % |
c ==============================================================================
c Found solution: 348069
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14396 |    8921    20980 |    2973    3077    43578    14.2 |  1.705 % |
c |     14496 |    8921    20980 |    3270    1639    16821    10.3 |  1.733 % |
c ==============================================================================
c Found solution: 346080
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14585 |    8930    21003 |    2976    1728    17989    10.4 |  1.733 % |
c |     14685 |    8930    21003 |    3273    1828    19860    10.9 |  1.761 % |
c |     14835 |    8930    21003 |    3600    1978    22834    11.5 |  1.760 % |
c |     15060 |    8930    21003 |    3961    2203    27004    12.3 |  1.760 % |
c |     15402 |    8930    21003 |    4357    2545    33751    13.3 |  1.760 % |
c |     15909 |    8930    21003 |    4792    3052    42187    13.8 |  1.760 % |
c ==============================================================================
c Found solution: 346053
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16247 |    8941    21034 |    2980    3390    47407    14.0 |  1.760 % |
c ==============================================================================
c Found solution: 345541
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16253 |    8953    21066 |    2984    1701    17861    10.5 |  1.760 % |
c |     16353 |    8953    21066 |    3282    1801    19982    11.1 |  1.814 % |
c |     16503 |    8953    21066 |    3610    1951    23189    11.9 |  1.815 % |
c |     16728 |    8953    21066 |    3971    2176    27434    12.6 |  1.814 % |
c |     17065 |    8953    21066 |    4368    2513    34906    13.9 |  1.814 % |
c |     17571 |    8953    21066 |    4805    3019    46530    15.4 |  1.814 % |
c |     18330 |    8953    21066 |    5286    3778    58445    15.5 |  1.814 % |
c ==============================================================================
c Found solution: 345540
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19242 |    8969    21106 |    2989    4690    83910    17.9 |  1.814 % |
c |     19342 |    8969    21106 |    3287    2445    39645    16.2 |  1.840 % |
c |     19492 |    8969    21106 |    3616    2595    42083    16.2 |  1.840 % |
c |     19718 |    8969    21106 |    3978    2821    47313    16.8 |  1.840 % |
c |     20055 |    8855    20853 |    4376    2816    47124    16.7 |  2.774 % |
c |     20561 |    8855    20853 |    4813    3322    56187    16.9 |  2.775 % |
c |     21323 |    8855    20853 |    5295    4084    68726    16.8 |  2.775 % |
c |     22462 |    8855    20853 |    5824    5223    92349    17.7 |  2.774 % |
c ==============================================================================
c Found solution: 345157
c ---[   0]---> Sorter-cost:  270     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22548 |    9477    22302 |    3159    5309    94646    17.8 |  2.774 % |
c |     22648 |    9477    22302 |    3474    2755    37055    13.5 |  2.628 % |
c |     22799 |    9477    22302 |    3822    2906    39665    13.6 |  2.628 % |
c |     23025 |    9477    22302 |    4204    3132    44507    14.2 |  2.628 % |
c |     23363 |    9477    22302 |    4625    3470    49689    14.3 |  2.628 % |
c |     23869 |    9477    22302 |    5087    3976    60472    15.2 |  2.628 % |
c ==============================================================================
c Found solution: 345059
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24518 |    9488    22329 |    3162    4625    72381    15.6 |  2.628 % |
c |     24619 |    9488    22329 |    3478    2414    29648    12.3 |  2.652 % |
c |     24770 |    9488    22329 |    3826    2565    32022    12.5 |  2.653 % |
c |     24996 |    9488    22329 |    4208    2791    37442    13.4 |  2.652 % |
c |     25335 |    9488    22329 |    4629    3130    45295    14.5 |  2.653 % |
c |     25841 |    9488    22329 |    5092    3636    56557    15.6 |  2.652 % |
c ==============================================================================
c Found solution: 345056
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26354 |    9365    22054 |    3121    3892    66095    17.0 |  2.652 % |
c |     26456 |    9365    22054 |    3433    2048    26720    13.0 |  3.748 % |
c ==============================================================================
c Found solution: 345018
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26573 |    9379    22088 |    3126    2165    28757    13.3 |  3.748 % |
c |     26673 |    9379    22088 |    3438    2265    31041    13.7 |  3.770 % |
c |     26823 |    9379    22088 |    3782    2415    32970    13.7 |  3.769 % |
c |     27048 |    9379    22088 |    4160    2640    38793    14.7 |  3.769 % |
c ==============================================================================
c Found solution: 345016
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27338 |    9397    22132 |    3132    2930    43585    14.9 |  3.769 % |
c |     27439 |    9397    22132 |    3445    3031    46113    15.2 |  3.789 % |
c ==============================================================================
c Found solution: 345014
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27499 |    9415    22175 |    3138    3091    46938    15.2 |  3.789 % |
c |     27599 |    9415    22175 |    3451    3191    49763    15.6 |  3.808 % |
c |     27750 |    9415    22175 |    3796    3342    52550    15.7 |  3.808 % |
c |     27976 |    9415    22175 |    4176    3568    57763    16.2 |  3.808 % |
c |     28313 |    9415    22175 |    4594    3905    65556    16.8 |  3.808 % |
c ==============================================================================
c Found solution: 344850
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28447 |    9433    22216 |    3144    4039    68103    16.9 |  3.808 % |
c |     28552 |    9433    22216 |    3458    2125    26155    12.3 |  3.827 % |
c |     28702 |    9433    22216 |    3804    2275    29161    12.8 |  3.827 % |
c |     28927 |    9433    22216 |    4184    2500    32831    13.1 |  3.827 % |
c |     29264 |    9433    22216 |    4603    2837    40707    14.3 |  3.827 % |
c ==============================================================================
c Found solution: 344846
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29426 |    9454    22264 |    3151    2999    44667    14.9 |  3.827 % |
c |     29527 |    9454    22264 |    3466    3100    47222    15.2 |  3.844 % |
c |     29678 |    9454    22264 |    3812    3251    49584    15.3 |  3.844 % |
c |     29904 |    9269    21851 |    4193    3221    49634    15.4 |  5.209 % |
c |     30241 |    9269    21851 |    4613    3558    57893    16.3 |  5.209 % |
c |     30747 |    9269    21851 |    5074    4064    67694    16.7 |  5.209 % |
c ==============================================================================
c Found solution: 344827
c ---[   0]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31182 |   10405    24498 |    3468    4499    75323    16.7 |  5.209 % |
c |     31288 |   10405    24498 |    3814    2356    25757    10.9 |  4.714 % |
c |     31440 |   10405    24498 |    4196    2508    29351    11.7 |  4.714 % |
c |     31665 |   10405    24498 |    4615    2733    35741    13.1 |  4.714 % |
c |     32003 |   10405    24498 |    5077    3071    45403    14.8 |  4.714 % |
c |     32509 |   10405    24498 |    5585    3577    59333    16.6 |  4.714 % |
c |     33269 |   10405    24498 |    6143    4337    76014    17.5 |  4.714 % |
c ==============================================================================
c Found solution: 344826
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33513 |   10421    24537 |    3473    4581    80851    17.6 |  4.714 % |
c |     33614 |   10421    24537 |    3820    2392    30228    12.6 |  4.731 % |
c |     33765 |   10421    24537 |    4202    2543    34190    13.4 |  4.731 % |
c |     33991 |   10421    24537 |    4622    2769    39429    14.2 |  4.731 % |
c |     34328 |   10421    24537 |    5084    3106    48004    15.5 |  4.731 % |
c |     34834 |   10421    24537 |    5593    3612    56272    15.6 |  4.731 % |
c |     35593 |   10421    24537 |    6152    4371    71560    16.4 |  4.731 % |
c ==============================================================================
c Found solution: 344820
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36257 |   10441    24582 |    3480    5035    87050    17.3 |  4.731 % |
c ==============================================================================
c Found solution: 344818
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36289 |   10455    24614 |    3485    2550    32881    12.9 |  4.731 % |
c |     36390 |   10455    24614 |    3833    2651    35561    13.4 |  4.764 % |
c |     36540 |   10455    24614 |    4216    2801    40258    14.4 |  4.764 % |
c ==============================================================================
c Found solution: 344816
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36615 |   10473    24655 |    3491    2876    41424    14.4 |  4.764 % |
c |     36719 |   10473    24655 |    3840    2980    43256    14.5 |  4.781 % |
c |     36869 |   10473    24655 |    4224    3130    46685    14.9 |  4.781 % |
c |     37095 |   10473    24655 |    4646    3356    50303    15.0 |  4.781 % |
c |     37432 |   10473    24655 |    5111    3693    57298    15.5 |  4.781 % |
c |     37938 |   10473    24655 |    5622    4199    68810    16.4 |  4.781 % |
c ==============================================================================
c Found solution: 344799
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38280 |   10488    24691 |    3496    4541    74852    16.5 |  4.781 % |
c |     38380 |   10488    24691 |    3845    2371    27110    11.4 |  4.798 % |
c |     38532 |   10488    24691 |    4230    2523    30322    12.0 |  4.798 % |
c |     38757 |   10488    24691 |    4653    2748    35294    12.8 |  4.798 % |
c ==============================================================================
c Found solution: 344796
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38938 |   10505    24733 |    3501    2929    38257    13.1 |  4.798 % |
c |     39040 |   10505    24733 |    3851    3031    40750    13.4 |  4.813 % |
c |     39190 |   10505    24733 |    4236    3181    44416    14.0 |  4.813 % |
c |     39416 |   10505    24733 |    4659    3407    46941    13.8 |  4.813 % |
c |     39754 |   10505    24733 |    5125    3745    51360    13.7 |  4.813 % |
c |     40260 |   10505    24733 |    5638    4251    60495    14.2 |  4.813 % |
c ==============================================================================
c Found solution: 344793
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40364 |   10520    24769 |    3506    4355    62857    14.4 |  4.813 % |
c |     40464 |   10520    24769 |    3856    2278    23960    10.5 |  4.829 % |
c |     40614 |   10520    24769 |    4242    2428    26268    10.8 |  4.829 % |
c |     40839 |   10520    24769 |    4666    2653    31485    11.9 |  4.829 % |
c ==============================================================================
c Found solution: 344792
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41084 |   10535    24805 |    3511    2898    35953    12.4 |  4.829 % |
c |     41185 |   10535    24805 |    3862    2999    37393    12.5 |  4.846 % |
c |     41336 |   10535    24805 |    4248    3150    40973    13.0 |  4.846 % |
c |     41561 |   10535    24805 |    4673    3375    44849    13.3 |  4.846 % |
c ==============================================================================
c Found solution: 344789
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41611 |   10550    24842 |    3516    3425    45810    13.4 |  4.846 % |
c ==============================================================================
c Found solution: 344788
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41628 |   10565    24878 |    3521    3442    46084    13.4 |  4.846 % |
c ==============================================================================
c Found solution: 344786
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41657 |   10580    24913 |    3526    3471    46615    13.4 |  4.846 % |
c |     41757 |   10580    24913 |    3878    3571    48575    13.6 |  4.894 % |
c ==============================================================================
c Found solution: 344785
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41833 |   10598    24956 |    3532    3647    49771    13.6 |  4.894 % |
c |     41933 |   10598    24956 |    3885    3747    51741    13.8 |  4.908 % |
c |     42085 |   10598    24956 |    4273    3899    54367    13.9 |  4.908 % |
c |     42310 |   10598    24956 |    4701    4124    57579    14.0 |  4.908 % |
c ==============================================================================
c Found solution: 344784
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42465 |   10615    24996 |    3538    4279    59647    13.9 |  4.908 % |
c |     42566 |   10615    24996 |    3891    2241    21409     9.6 |  4.923 % |
c |     42716 |   10615    24996 |    4280    2391    24371    10.2 |  4.923 % |
c |     42941 |   10615    24996 |    4709    2616    28310    10.8 |  4.923 % |
c |     43278 |   10615    24996 |    5179    2953    36099    12.2 |  4.923 % |
c ==============================================================================
c Found solution: 344783
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43458 |   10633    25039 |    3544    3133    39095    12.5 |  4.923 % |
c |     43561 |   10633    25039 |    3898    3236    40821    12.6 |  4.936 % |
c |     43713 |   10633    25039 |    4288    3388    43520    12.8 |  4.937 % |
c ==============================================================================
c Found solution: 344781
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43721 |   10653    25086 |    3551    3396    43617    12.8 |  4.937 % |
c ==============================================================================
c Found solution: 344779
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43726 |   10670    25126 |    3556    3401    43693    12.8 |  4.937 % |
c ==============================================================================
c Found solution: 344775
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43737 |   10687    25166 |    3562    3412    43874    12.9 |  4.937 % |
c ==============================================================================
c Found solution: 344774
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43807 |   10704    25206 |    3568    3482    46407    13.3 |  4.937 % |
c |     43909 |   10704    25206 |    3924    3584    48204    13.4 |  4.993 % |
c ==============================================================================
c Found solution: 344771
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43950 |   10719    25241 |    3573    3625    48855    13.5 |  4.993 % |
c |     44050 |   10719    25241 |    3930    3725    50529    13.6 |  5.009 % |
c |     44200 |   10719    25241 |    4323    3875    53661    13.8 |  5.009 % |
c ==============================================================================
c Found solution: 344766
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44222 |   10737    25283 |    3579    3897    54491    14.0 |  5.009 % |
c ==============================================================================
c Found solution: 344765
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44252 |   10755    25325 |    3585    1979    19086     9.6 |  5.009 % |
c |     44352 |   10755    25325 |    3943    2079    20662     9.9 |  5.035 % |
c |     44503 |   10755    25325 |    4337    2230    23422    10.5 |  5.035 % |
c |     44729 |   10755    25325 |    4771    2456    27555    11.2 |  5.035 % |
c ==============================================================================
c Found solution: 344764
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44918 |   10773    25368 |    3591    2645    31294    11.8 |  5.035 % |
c |     45018 |   10773    25368 |    3950    2745    33066    12.0 |  5.048 % |
c ==============================================================================
c Found solution: 344763
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45041 |   10790    25407 |    3596    2768    33482    12.1 |  5.048 % |
c ==============================================================================
c Found solution: 344757
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45055 |   10808    25449 |    3602    2782    33894    12.2 |  5.048 % |
c |     45158 |   10808    25449 |    3962    2885    35341    12.2 |  5.076 % |
c ==============================================================================
c Found solution: 344756
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45188 |   10825    25488 |    3608    2915    35978    12.3 |  5.076 % |
c ==============================================================================
c Found solution: 344755
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45263 |   10842    25527 |    3614    2990    36745    12.3 |  5.076 % |
c ==============================================================================
c Found solution: 344754
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45271 |   10859    25566 |    3619    2998    36997    12.3 |  5.076 % |
c |     45372 |   10859    25566 |    3980    3099    38253    12.3 |  5.118 % |
c |     45522 |   10859    25566 |    4378    3249    40622    12.5 |  5.118 % |
c ==============================================================================
c Found solution: 344752
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45701 |   10876    25605 |    3625    3428    44183    12.9 |  5.118 % |
c |     45801 |   10876    25605 |    3987    3528    45577    12.9 |  5.132 % |
c |     45951 |   10876    25605 |    4386    3678    47750    13.0 |  5.132 % |
c ==============================================================================
c Found solution: 344751
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45959 |   10893    25644 |    3631    3686    47880    13.0 |  5.132 % |
c |     46059 |   10893    25644 |    3994    3786    49618    13.1 |  5.146 % |
c ==============================================================================
c Found solution: 344750
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46153 |   10910    25683 |    3636    3880    51517    13.3 |  5.146 % |
c |     46253 |   10910    25683 |    3999    2040    18747     9.2 |  5.160 % |
c |     46403 |   10910    25683 |    4399    2190    21504     9.8 |  5.160 % |
c |     46628 |   10585    24949 |    4839    1499     9418     6.3 |  7.195 % |
c ==============================================================================
c Optimal solution: 344750
s OPTIMUM FOUND
v VOL1_bit_10 -VOL1_bit_9 VOL1_bit_8 -VOL1_bit_7 VOL1_bit_6 -VOL1_bit_5 VOL1_bit_4 -VOL1_bit_3 VOL1_bit_2 -VOL1_bit_1 VOL1_bit0 VOL1_bit1 -VOL1_bit2 -VOL1_bit3 -VOL1_bit4 -VOL1_bit5 -VOL1_bit6 -VOL1_bit7 -VOL1_bit8 -VOL1_bit9 -VOL1_bit10 -VOL1_bit11 -VOL1_bit12 -VOL1_bit13 -VOL1_bit14 -VOL1_bit15 -VOL1_bit16 -VOL1_bit17 -VOL1_bit18 -VOL1_bit19 VOL2_bit_10 -VOL2_bit_9 VOL2_bit_8 -VOL2_bit_7 VOL2_bit_6 -VOL2_bit_5 VOL2_bit_4 -VOL2_bit_3 VOL2_bit_2 -VOL2_bit_1 VOL2_bit0 -VOL2_bit1 VOL2_bit2 VOL2_bit3 -VOL2_bit4 -VOL2_bit5 -VOL2_bit6 -VOL2_bit7 -VOL2_bit8 -VOL2_bit9 -VOL2_bit10 -VOL2_bit11 -VOL2_bit12 -VOL2_bit13 -VOL2_bit14 -VOL2_bit15 -VOL2_bit16 -VOL2_bit17 -VOL2_bit18 -VOL2_bit19 -VOL3_bit_10 -VOL3_bit_9 -VOL3_bit_8 -VOL3_bit_7 -VOL3_bit_6 -VOL3_bit_5 -VOL3_bit_4 -VOL3_bit_3 -VOL3_bit_2 -VOL3_bit_1 -VOL3_bit0 VOL3_bit1 VOL3_bit2 VOL3_bit3 VOL3_bit4 VOL4_bit_10 -VOL4_bit_9 -VOL4_bit_8 -VOL4_bit_7 -VOL4_bit_6 -VOL4_bit_5 -VOL4_bit_4 -VOL4_bit_3 -VOL4_bit_2 -VOL4_bit_1 -VOL4_bit0 -VOL4_bit1 -VOL4_bit2 -VOL4_bit3 -VOL4_bit4
c _______________________________________________________________________________
c 
c restarts              : 222
c conflicts             : 46726          (1513 /sec)
c decisions             : 78990          (2558 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 30.8763 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/12421/stat): 12421 (minisat+_script) R 12420 12421 20602 0 -1 0 19 0 0 0 0 0 0 0 24 0 1 0 1732198193 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/12421/statm): 174 9 169 147 0 27 0
[pid=12421] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=12422
New process pid=12423
New process pid=12424
execve syscall for /bin/sed executable
One traced child (pid=12423) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=12424) exited with status: 0
One traced child (pid=12422) exited with status: 0
New process pid=12425
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-maros.opb

[startup+10.0029 s]
Raw data (loadavg): 0.93 0.96 0.91 2/58 12425
Raw data (/proc/12421/stat): 12421 (minisat+_script) S 12420 12421 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732198193 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12421/statm): 531 226 485 147 0 384 0
[pid=12421] vsize: 2124
Raw data (/proc/12425/stat): 12425 (minisat+_64-bit) R 12421 12421 20602 0 -1 0 556 0 0 0 989 2 0 0 25 0 1 0 1732198198 2646016 543 4294967295 134512640 135094434 3221224432 3221223024 134551421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12425/statm): 646 543 145 145 0 501 0
[pid=12425] vsize: 2584
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 4708

[startup+20.0036 s]
Raw data (loadavg): 0.94 0.96 0.91 2/58 12425
Raw data (/proc/12421/stat): 12421 (minisat+_script) S 12420 12421 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732198193 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12421/statm): 531 226 485 147 0 384 0
[pid=12421] vsize: 2124
Raw data (/proc/12425/stat): 12425 (minisat+_64-bit) R 12421 12421 20602 0 -1 0 624 0 0 0 1987 3 0 0 25 0 1 0 1732198198 2916352 611 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12425/statm): 712 611 145 145 0 567 0
[pid=12425] vsize: 2848
Current children cumulated CPU time (s) 19.9
Current children cumulated vsize (Kb) 4972

[startup+30.0053 s]
Raw data (loadavg): 0.95 0.96 0.91 2/58 12425
Raw data (/proc/12421/stat): 12421 (minisat+_script) S 12420 12421 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732198193 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12421/statm): 531 226 485 147 0 384 0
[pid=12421] vsize: 2124
Raw data (/proc/12425/stat): 12425 (minisat+_64-bit) R 12421 12421 20602 0 -1 0 696 0 0 0 2985 4 0 0 25 0 1 0 1732198198 3350528 683 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12425/statm): 818 683 145 145 0 673 0
[pid=12425] vsize: 3272
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 5396
One traced child (pid=12425) exited with status: 30
One traced child (pid=12421) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 31.0414
CPU time (s): 30.9553
CPU user time (s): 30.8833
CPU system time (s): 0.071989
CPU usage (%): 99.7225
Max. virtual memory (cumulated for all children) (Kb): 5396

Verifier Data

Verifier:	OK	344750