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-13-7/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-13-7-maros.opb
MD5SUM1ae5b04b2d0e1f5ab82e29e98b8350c0
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 43097
Optimality of the best value was proved YES
Number of terms in the objective function 64
Biggest coefficient in the objective function 4718592
Number of bits for the biggest coefficient in the objective function 23
Sum of the numbers in the objective function 14745570
Number of bits of the sum of numbers in the objective function 24
Biggest number in a constraint 4718592
Number of bits of the biggest number in a constraint 23
Biggest sum of numbers in a constraint 14745570
Number of bits of the biggest sum of numbers24
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark23.3694
Number of variables64
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 constraint12
Maximum length of a constraint64

Trace number 6321

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        868140 kB
Buffers:         24944 kB
Cached:         115348 kB
SwapCached:        876 kB
Active:          40268 kB
Inactive:       102788 kB
HighTotal:      131008 kB
HighFree:        20552 kB
LowTotal:       903652 kB
LowFree:        847588 kB
SwapTotal:     2097136 kB
SwapFree:      2095848 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            17904 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:53:55 (client local time) WITH STATUS 30 IN 23.3694 SECONDS
stats: 3515 0 23.3694 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:   11
c ---[   3]---> Sorter-cost:  961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  410     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4455    10455 |    1485       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 54221
c ---[   0]---> Sorter-cost:  988     Base: 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 |        94 |    6727    15762 |    2242      94     1453    15.5 |  0.000 % |
c ==============================================================================
c Found solution: 53679
c ---[   0]---> Sorter-cost:   12     Base: 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 |       111 |    6745    15831 |    2248     111     1578    14.2 |  0.000 % |
c ==============================================================================
c Found solution: 49212
c ---[   0]---> Sorter-cost:   14     Base: 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 |       139 |    6773    15898 |    2257     139     1822    13.1 |  0.000 % |
c |       239 |    6773    15898 |    2482     239     3347    14.0 |  1.048 % |
c |       390 |    6773    15898 |    2730     390     5135    13.2 |  1.049 % |
c |       618 |    6773    15898 |    3004     618     8483    13.7 |  1.048 % |
c |       955 |    6773    15898 |    3304     955    15439    16.2 |  1.049 % |
c |      1461 |    6773    15898 |    3634    1461    23005    15.7 |  1.049 % |
c ==============================================================================
c Found solution: 49121
c ---[   0]---> Sorter-cost:   13     Base: 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 |      1506 |    6779    15924 |    2259    1506    23500    15.6 |  1.049 % |
c |      1606 |    6779    15924 |    2484    1606    24721    15.4 |  1.087 % |
c ==============================================================================
c Found solution: 47761
c ---[   0]---> Sorter-cost:   11     Base: 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 |      1618 |    6796    15965 |    2265    1618    24822    15.3 |  1.087 % |
c |      1718 |    6796    15965 |    2491    1718    27411    16.0 |  1.122 % |
c |      1869 |    6796    15965 |    2740    1869    30380    16.3 |  1.123 % |
c |      2095 |    6796    15965 |    3014    2095    35545    17.0 |  1.122 % |
c ==============================================================================
c Found solution: 47583
c ---[   0]---> Sorter-cost:   11     Base: 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 |      2375 |    6805    15990 |    2268    2375    41355    17.4 |  1.122 % |
c |      2476 |    6802    15984 |    2494    1287    20378    15.8 |  1.201 % |
c |      2627 |    6802    15984 |    2744    1438    22436    15.6 |  1.200 % |
c ==============================================================================
c Found solution: 47072
c ---[   0]---> Sorter-cost:   13     Base: 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 |      2802 |    6811    16012 |    2270    1613    24999    15.5 |  1.200 % |
c |      2902 |    6811    16012 |    2497    1713    27087    15.8 |  1.240 % |
c |      3052 |    6811    16012 |    2746    1863    29554    15.9 |  1.238 % |
c ==============================================================================
c Found solution: 46956
c ---[   0]---> Sorter-cost:   11     Base: 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 |      3077 |    6822    16040 |    2274    1888    30004    15.9 |  1.238 % |
c ==============================================================================
c Found solution: 46814
c ---[   0]---> Sorter-cost:   14     Base: 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 |      3107 |    6836    16077 |    2278    1918    30451    15.9 |  1.238 % |
c ==============================================================================
c Found solution: 46810
c ---[   0]---> Sorter-cost:   13     Base: 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 |      3132 |    6848    16109 |    2282    1943    30841    15.9 |  1.238 % |
c |      3232 |    6848    16109 |    2510    2043    32526    15.9 |  1.347 % |
c |      3382 |    6848    16109 |    2761    2193    34455    15.7 |  1.347 % |
c |      3608 |    6848    16109 |    3037    2419    37161    15.4 |  1.347 % |
c ==============================================================================
c Found solution: 46758
c ---[   0]---> Sorter-cost:   12     Base: 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 |      3671 |    6861    16140 |    2287    2482    38274    15.4 |  1.347 % |
c |      3772 |    6861    16140 |    2515    1342    14247    10.6 |  1.384 % |
c ==============================================================================
c Found solution: 45478
c ---[   0]---> Sorter-cost:    7     Base: 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 |      3782 |    6869    16158 |    2289    1352    14384    10.6 |  1.384 % |
c |      3884 |    6869    16158 |    2517    1454    16340    11.2 |  1.421 % |
c |      4039 |    6869    16158 |    2769    1609    18375    11.4 |  1.421 % |
c |      4265 |    6869    16158 |    3046    1835    21428    11.7 |  1.421 % |
c ==============================================================================
c Found solution: 45262
c ---[   0]---> Sorter-cost:   11     Base: 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 |      4347 |    6881    16187 |    2293    1917    23553    12.3 |  1.421 % |
c |      4452 |    6881    16187 |    2522    2022    24947    12.3 |  1.458 % |
c |      4602 |    6881    16187 |    2774    2172    27451    12.6 |  1.458 % |
c |      4828 |    6881    16187 |    3051    2398    30681    12.8 |  1.458 % |
c |      5167 |    6881    16187 |    3357    2737    36497    13.3 |  1.458 % |
c |      5675 |    6881    16187 |    3692    3245    45663    14.1 |  1.458 % |
c |      6434 |    6881    16187 |    4062    2014    26572    13.2 |  1.458 % |
c |      7575 |    6881    16187 |    4468    3155    45341    14.4 |  1.458 % |
c ==============================================================================
c Found solution: 45261
c ---[   0]---> Sorter-cost:    7     Base: 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 |      8894 |    6890    16209 |    2296    4474    73429    16.4 |  1.458 % |
c ==============================================================================
c Found solution: 44828
c ---[   0]---> Sorter-cost:   10     Base: 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 |      8914 |    6901    16240 |    2300    2257    32085    14.2 |  1.458 % |
c |      9015 |    6901    16240 |    2530    2358    33311    14.1 |  1.531 % |
c |      9165 |    6901    16240 |    2783    2508    36275    14.5 |  1.531 % |
c |      9391 |    6901    16240 |    3061    2734    39188    14.3 |  1.531 % |
c |      9730 |    6901    16240 |    3367    3073    44267    14.4 |  1.531 % |
c |     10237 |    6901    16240 |    3704    3580    54280    15.2 |  1.531 % |
c |     11000 |    6901    16240 |    4074    2394    29965    12.5 |  1.531 % |
c |     12141 |    6901    16240 |    4482    3535    51793    14.7 |  1.531 % |
c ==============================================================================
c Found solution: 44769
c ---[   0]---> Sorter-cost:    7     Base: 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 |     13520 |    6908    16263 |    2302    2556    27442    10.7 |  1.531 % |
c |     13621 |    6908    16263 |    2532    1379    10990     8.0 |  1.567 % |
c |     13771 |    6908    16263 |    2785    1529    13596     8.9 |  1.567 % |
c |     13996 |    6908    16263 |    3063    1754    17123     9.8 |  1.567 % |
c ==============================================================================
c Found solution: 44721
c ---[   0]---> Sorter-cost:   10     Base: 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 |     14120 |    6917    16288 |    2305    1878    18313     9.8 |  1.567 % |
c ==============================================================================
c Found solution: 44449
c ---[   0]---> Sorter-cost:    9     Base: 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 |     14132 |    6927    16316 |    2309    1890    18602     9.8 |  1.567 % |
c |     14234 |    6927    16316 |    2539    1992    20732    10.4 |  1.637 % |
c ==============================================================================
c Found solution: 44293
c ---[   0]---> Sorter-cost:   12     Base: 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 |     14349 |    6941    16350 |    2313    2107    23370    11.1 |  1.637 % |
c |     14449 |    6941    16350 |    2544    2207    25213    11.4 |  1.671 % |
c |     14600 |    6941    16350 |    2798    2358    27396    11.6 |  1.671 % |
c |     14825 |    6941    16350 |    3078    2583    30696    11.9 |  1.671 % |
c |     15162 |    6941    16350 |    3386    2920    36694    12.6 |  1.671 % |
c |     15668 |    6941    16350 |    3725    3426    45563    13.3 |  1.671 % |
c ==============================================================================
c Found solution: 44052
c ---[   0]---> Sorter-cost:   12     Base: 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 |     15868 |    6953    16380 |    2317    3626    50124    13.8 |  1.671 % |
c |     15969 |    6953    16380 |    2548    1914    20129    10.5 |  1.706 % |
c |     16121 |    6953    16380 |    2803    2066    21969    10.6 |  1.706 % |
c |     16347 |    6953    16380 |    3083    2292    26233    11.4 |  1.706 % |
c ==============================================================================
c Found solution: 44048
c ---[   0]---> Sorter-cost:   11     Base: 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 |     16545 |    6966    16413 |    2322    2490    29607    11.9 |  1.706 % |
c |     16648 |    6966    16413 |    2554    1348    11205     8.3 |  1.740 % |
c |     16798 |    6966    16413 |    2809    1498    13726     9.2 |  1.740 % |
c |     17025 |    6966    16413 |    3090    1725    17757    10.3 |  1.740 % |
c |     17365 |    6947    16371 |    3399    2064    22105    10.7 |  1.933 % |
c |     17874 |    6947    16371 |    3739    2573    31541    12.3 |  1.933 % |
c |     18634 |    6947    16371 |    4113    3333    43616    13.1 |  1.933 % |
c ==============================================================================
c Found solution: 44046
c ---[   0]---> Sorter-cost:    9     Base: 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 |     19334 |    6957    16396 |    2319    4033    55712    13.8 |  1.933 % |
c |     19438 |    6957    16396 |    2550    2121    23415    11.0 |  1.968 % |
c |     19591 |    6957    16396 |    2805    2274    25207    11.1 |  1.968 % |
c ==============================================================================
c Found solution: 44044
c ---[   0]---> Sorter-cost:   10     Base: 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 |     19787 |    6969    16425 |    2323    2470    27993    11.3 |  1.968 % |
c |     19887 |    6969    16425 |    2555    1335    10218     7.7 |  2.002 % |
c ==============================================================================
c Found solution: 44034
c ---[   0]---> Sorter-cost:   12     Base: 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 |     19982 |    6980    16453 |    2326    1430    12648     8.8 |  2.002 % |
c |     20082 |    6980    16453 |    2558    1530    13615     8.9 |  2.037 % |
c |     20232 |    6891    16251 |    2814    1506    13776     9.1 |  3.035 % |
c |     20458 |    6891    16251 |    3095    1732    15889     9.2 |  3.037 % |
c ==============================================================================
c Found solution: 44025
c ---[   0]---> Sorter-cost:   12     Base: 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 |     20513 |    6843    16144 |    2281    1453    12699     8.7 |  3.037 % |
c |     20614 |    6843    16144 |    2509    1554    14048     9.0 |  3.755 % |
c ==============================================================================
c Found solution: 44006
c ---[   0]---> Sorter-cost:    9     Base: 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 |     20693 |    6852    16166 |    2284    1633    15691     9.6 |  3.755 % |
c |     20793 |    6852    16166 |    2512    1733    17138     9.9 |  3.788 % |
c |     20943 |    6852    16166 |    2763    1883    19668    10.4 |  3.788 % |
c |     21168 |    6852    16166 |    3040    2108    23643    11.2 |  3.788 % |
c |     21506 |    6852    16166 |    3344    2446    29003    11.9 |  3.788 % |
c ==============================================================================
c Found solution: 44004
c ---[   0]---> Sorter-cost:   11     Base: 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 |     21585 |    6863    16192 |    2287    2525    30129    11.9 |  3.788 % |
c ==============================================================================
c Found solution: 44003
c ---[   0]---> Sorter-cost:    4     Base: 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 |     21600 |    6867    16203 |    2289    1278     9814     7.7 |  3.788 % |
c ==============================================================================
c Found solution: 43993
c ---[   0]---> Sorter-cost:   10     Base: 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 |     21604 |    6874    16225 |    2291    1282     9859     7.7 |  3.788 % |
c ==============================================================================
c Found solution: 43934
c ---[   0]---> Sorter-cost:    9     Base: 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 |     21608 |    6884    16253 |    2294    1286     9892     7.7 |  3.788 % |
c ==============================================================================
c Found solution: 43669
c ---[   0]---> Sorter-cost:   11     Base: 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 |     21617 |    6899    16290 |    2299    1295    10077     7.8 |  3.788 % |
c ==============================================================================
c Found solution: 43661
c ---[   0]---> Sorter-cost:    9     Base: 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 |     21633 |    6912    16322 |    2304    1311    10473     8.0 |  3.788 % |
c ==============================================================================
c Found solution: 43486
c ---[   0]---> Sorter-cost:    7     Base: 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 |     21710 |    6920    16342 |    2306    1388    11165     8.0 |  3.788 % |
c |     21810 |    6920    16342 |    2536    1488    13394     9.0 |  3.990 % |
c |     21960 |    6920    16342 |    2790    1638    15643     9.6 |  3.990 % |
c |     22187 |    6920    16342 |    3069    1865    19235    10.3 |  3.990 % |
c |     22524 |    6920    16342 |    3376    2202    24208    11.0 |  3.990 % |
c ==============================================================================
c Found solution: 43484
c ---[   0]---> Sorter-cost:    9     Base: 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 |     22933 |    6928    16364 |    2309    2611    29688    11.4 |  3.990 % |
c |     23034 |    6928    16364 |    2539    1407    11887     8.4 |  4.020 % |
c |     23184 |    6928    16364 |    2793    1557    14910     9.6 |  4.020 % |
c ==============================================================================
c Found solution: 43482
c ---[   0]---> Sorter-cost:    7     Base: 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 |     23277 |    6936    16384 |    2312    1650    16240     9.8 |  4.020 % |
c |     23378 |    6936    16384 |    2543    1751    17937    10.2 |  4.050 % |
c |     23530 |    6936    16384 |    2797    1903    20380    10.7 |  4.050 % |
c |     23756 |    6936    16384 |    3077    2129    24543    11.5 |  4.050 % |
c |     24094 |    6936    16384 |    3384    2467    30002    12.2 |  4.050 % |
c ==============================================================================
c Found solution: 43459
c ---[   0]---> Sorter-cost:    9     Base: 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 |     24222 |    6944    16406 |    2314    2595    32414    12.5 |  4.050 % |
c |     24322 |    6944    16406 |    2545    1398    12737     9.1 |  4.079 % |
c |     24474 |    6944    16406 |    2799    1550    15698    10.1 |  4.079 % |
c |     24700 |    6944    16406 |    3079    1776    21704    12.2 |  4.079 % |
c |     25037 |    6944    16406 |    3387    2113    27209    12.9 |  4.080 % |
c |     25544 |    6944    16406 |    3726    2620    36137    13.8 |  4.080 % |
c |     26303 |    6944    16406 |    4099    3379    52722    15.6 |  4.080 % |
c ==============================================================================
c Found solution: 43458
c ---[   0]---> Sorter-cost:    9     Base: 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 |     26492 |    6954    16432 |    2318    3568    57336    16.1 |  4.080 % |
c |     26593 |    6954    16432 |    2549    1885    23996    12.7 |  4.108 % |
c |     26744 |    6954    16432 |    2804    2036    26513    13.0 |  4.108 % |
c ==============================================================================
c Found solution: 43457
c ---[   0]---> Sorter-cost:   10     Base: 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 |     26790 |    6965    16461 |    2321    2082    27489    13.2 |  4.108 % |
c ==============================================================================
c Found solution: 43450
c ---[   0]---> Sorter-cost:   10     Base: 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 |     26801 |    6976    16490 |    2325    2093    27619    13.2 |  4.108 % |
c ==============================================================================
c Found solution: 43448
c ---[   0]---> Sorter-cost:   12     Base: 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 |     26802 |    6990    16526 |    2330    2094    27687    13.2 |  4.108 % |
c ==============================================================================
c Found solution: 43443
c ---[   0]---> Sorter-cost:   10     Base: 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 |     26874 |    7000    16552 |    2333    2166    28924    13.4 |  4.108 % |
c |     26974 |    7000    16552 |    2566    2266    31765    14.0 |  4.211 % |
c |     27124 |    7000    16552 |    2822    2416    34979    14.5 |  4.211 % |
c |     27351 |    7000    16552 |    3105    2643    39418    14.9 |  4.211 % |
c |     27689 |    7000    16552 |    3415    2981    46999    15.8 |  4.212 % |
c |     28197 |    7000    16552 |    3757    3489    55560    15.9 |  4.211 % |
c ==============================================================================
c Found solution: 43209
c ---[   0]---> Sorter-cost:   11     Base: 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 |     28793 |    7011    16580 |    2337    4085    66559    16.3 |  4.211 % |
c |     28895 |    7011    16580 |    2570    2145    25876    12.1 |  4.239 % |
c |     29045 |    7011    16580 |    2827    2295    28083    12.2 |  4.239 % |
c |     29270 |    7011    16580 |    3110    2520    31760    12.6 |  4.239 % |
c |     29610 |    7011    16580 |    3421    2860    37337    13.1 |  4.239 % |
c ==============================================================================
c Found solution: 43206
c ---[   0]---> Sorter-cost:   10     Base: 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 |     29717 |    7023    16610 |    2341    2967    38797    13.1 |  4.239 % |
c |     29818 |    7023    16610 |    2575    1585    14362     9.1 |  4.267 % |
c |     29968 |    7023    16610 |    2832    1735    16833     9.7 |  4.266 % |
c ==============================================================================
c Found solution: 43205
c ---[   0]---> Sorter-cost:    9     Base: 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 |     30043 |    7032    16633 |    2344    1810    18082    10.0 |  4.266 % |
c |     30143 |    7032    16633 |    2578    1910    19927    10.4 |  4.295 % |
c |     30294 |    7032    16633 |    2836    2061    23204    11.3 |  4.295 % |
c |     30523 |    7032    16633 |    3119    2290    26886    11.7 |  4.295 % |
c ==============================================================================
c Found solution: 43198
c ---[   0]---> Sorter-cost:   10     Base: 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 |     30764 |    7044    16663 |    2348    2531    32302    12.8 |  4.295 % |
c |     30866 |    7044    16663 |    2582    1368    12482     9.1 |  4.321 % |
c |     31017 |    6806    16139 |    2841    1415    13491     9.5 |  6.591 % |
c |     31242 |    6806    16139 |    3125    1640    16844    10.3 |  6.591 % |
c ==============================================================================
c Found solution: 43195
c ---[   0]---> Sorter-cost:  270     Base: 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 |     31554 |    7426    17584 |    2475    1952    23389    12.0 |  6.591 % |
c |     31654 |    7426    17584 |    2722    2052    26063    12.7 |  6.127 % |
c |     31804 |    7426    17584 |    2994    2202    28729    13.0 |  6.127 % |
c ==============================================================================
c Found solution: 43193
c ---[   0]---> Sorter-cost:   10     Base: 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 |     31912 |    7440    17619 |    2480    2310    30666    13.3 |  6.127 % |
c |     32012 |    7440    17619 |    2728    2410    33465    13.9 |  6.147 % |
c |     32167 |    7440    17619 |    3000    2565    36033    14.0 |  6.147 % |
c |     32394 |    7440    17619 |    3300    2792    41647    14.9 |  6.147 % |
c |     32731 |    7440    17619 |    3630    3129    46532    14.9 |  6.147 % |
c ==============================================================================
c Found solution: 43192
c ---[   0]---> Sorter-cost:    8     Base: 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 |     33234 |    7451    17645 |    2483    3632    56206    15.5 |  6.147 % |
c |     33336 |    7451    17645 |    2731    1918    20584    10.7 |  6.170 % |
c |     33486 |    7451    17645 |    3004    2068    23457    11.3 |  6.170 % |
c |     33712 |    7451    17645 |    3304    2294    28676    12.5 |  6.170 % |
c |     34052 |    7451    17645 |    3635    2634    34288    13.0 |  6.170 % |
c ==============================================================================
c Found solution: 43185
c ---[   0]---> Sorter-cost:    7     Base: 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 |     34413 |    7460    17665 |    2486    2995    40845    13.6 |  6.170 % |
c ==============================================================================
c Found solution: 43166
c ---[   0]---> Sorter-cost:    8     Base: 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 |     34486 |    7471    17690 |    2490    1571    15304     9.7 |  6.170 % |
c ==============================================================================
c Found solution: 43164
c ---[   0]---> Sorter-cost:    9     Base: 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 |     34571 |    7484    17719 |    2494    1656    16627    10.0 |  6.170 % |
c |     34674 |    7484    17719 |    2743    1759    18442    10.5 |  6.240 % |
c |     34824 |    7484    17719 |    3017    1909    20550    10.8 |  6.240 % |
c ==============================================================================
c Found solution: 43163
c ---[   0]---> Sorter-cost:   11     Base: 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 |     34996 |    7498    17751 |    2499    2081    23759    11.4 |  6.240 % |
c |     35096 |    7498    17751 |    2748    2181    25672    11.8 |  6.259 % |
c |     35250 |    7498    17751 |    3023    2335    28041    12.0 |  6.258 % |
c |     35475 |    7498    17751 |    3326    2560    32431    12.7 |  6.259 % |
c |     35812 |    7498    17751 |    3658    2897    37778    13.0 |  6.259 % |
c ==============================================================================
c Found solution: 43157
c ---[   0]---> Sorter-cost:    7     Base: 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 |     36054 |    7507    17771 |    2502    3139    41189    13.1 |  6.259 % |
c |     36154 |    7422    17583 |    2752    1350    10584     7.8 |  7.052 % |
c |     36307 |    7422    17583 |    3027    1503    12765     8.5 |  7.053 % |
c ==============================================================================
c Found solution: 43152
c ---[   0]---> Sorter-cost:  461     Base: 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 |     36467 |    8553    20218 |    2851    1663    16026     9.6 |  7.053 % |
c |     36567 |    8553    20218 |    3136    1763    18222    10.3 |  6.257 % |
c |     36717 |    8553    20218 |    3449    1913    21711    11.3 |  6.258 % |
c |     36944 |    8553    20218 |    3794    2140    26141    12.2 |  6.258 % |
c ==============================================================================
c Found solution: 43151
c ---[   0]---> Sorter-cost:   11     Base: 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 |     37007 |    8571    20265 |    2857    2203    27326    12.4 |  6.258 % |
c |     37107 |    8571    20265 |    3142    2303    28750    12.5 |  6.269 % |
c ==============================================================================
c Found solution: 43150
c ---[   0]---> Sorter-cost:    9     Base: 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 |     37179 |    8584    20294 |    2861    2375    30447    12.8 |  6.269 % |
c |     37282 |    8584    20294 |    3147    2478    33829    13.7 |  6.287 % |
c ==============================================================================
c Found solution: 43149
c ---[   0]---> Sorter-cost:    9     Base: 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 |     37360 |    8595    20319 |    2865    2556    34895    13.7 |  6.287 % |
c |     37461 |    8595    20319 |    3151    2657    37342    14.1 |  6.307 % |
c |     37611 |    8595    20319 |    3466    2807    40703    14.5 |  6.308 % |
c ==============================================================================
c Found solution: 43133
c ---[   0]---> Sorter-cost:   12     Base: 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 |     37820 |    8610    20353 |    2870    3016    45156    15.0 |  6.308 % |
c |     37920 |    8610    20353 |    3157    3116    47536    15.3 |  6.323 % |
c ==============================================================================
c Found solution: 43130
c ---[   0]---> Sorter-cost:   10     Base: 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 |     38028 |    8623    20382 |    2874    3224    49014    15.2 |  6.323 % |
c |     38128 |    8623    20382 |    3161    1712    18271    10.7 |  6.341 % |
c |     38279 |    8623    20382 |    3477    1863    20949    11.2 |  6.342 % |
c |     38506 |    8623    20382 |    3825    2090    24586    11.8 |  6.341 % |
c ==============================================================================
c Found solution: 43129
c ---[   0]---> Sorter-cost:    9     Base: 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 |     38653 |    8636    20411 |    2878    2237    27363    12.2 |  6.341 % |
c ==============================================================================
c Found solution: 43128
c ---[   0]---> Sorter-cost:   10     Base: 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 |     38656 |    8649    20440 |    2883    2240    27404    12.2 |  6.341 % |
c ==============================================================================
c Found solution: 43127
c ---[   0]---> Sorter-cost:   13     Base: 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 |     38742 |    8666    20478 |    2888    2326    28603    12.3 |  6.341 % |
c ==============================================================================
c Found solution: 43106
c ---[   0]---> Sorter-cost:   11     Base: 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 |     38786 |    8678    20506 |    2892    2370    29448    12.4 |  6.341 % |
c |     38886 |    8678    20506 |    3181    2470    31315    12.7 |  6.412 % |
c |     39038 |    8678    20506 |    3499    2622    34693    13.2 |  6.412 % |
c |     39263 |    8678    20506 |    3849    2847    38634    13.6 |  6.412 % |
c |     39602 |    8678    20506 |    4234    3186    44693    14.0 |  6.412 % |
c ==============================================================================
c Found solution: 43104
c ---[   0]---> Sorter-cost:    9     Base: 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 |     39707 |    8690    20535 |    2896    3291    45984    14.0 |  6.412 % |
c |     39807 |    8690    20535 |    3185    1746    16737     9.6 |  6.431 % |
c ==============================================================================
c Found solution: 43103
c ---[   0]---> Sorter-cost:    9     Base: 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 |     39893 |    8702    20564 |    2900    1832    17762     9.7 |  6.431 % |
c ==============================================================================
c Found solution: 43101
c ---[   0]---> Sorter-cost:   11     Base: 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 |     39912 |    8714    20592 |    2904    1851    18000     9.7 |  6.431 % |
c ==============================================================================
c Found solution: 43100
c ---[   0]---> Sorter-cost:    9     Base: 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 |     39971 |    8726    20619 |    2908    1910    19127    10.0 |  6.431 % |
c |     40071 |    8726    20619 |    3198    2010    21004    10.4 |  6.490 % |
c ==============================================================================
c Found solution: 43097
c ---[   0]---> Sorter-cost:    9     Base: 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 |     40081 |    8738    20647 |    2912    2020    21247    10.5 |  6.490 % |
c |     40181 |    8738    20647 |    3203    2120    22592    10.7 |  6.509 % |
c |     40332 |    8738    20647 |    3523    2271    26073    11.5 |  6.509 % |
c |     40558 |    8738    20647 |    3875    2497    29653    11.9 |  6.509 % |
c ==============================================================================
c Optimal solution: 43097
s OPTIMUM FOUND
v -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 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 -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_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              : 205
c conflicts             : 40757          (1749 /sec)
c decisions             : 67646          (2903 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 23.3005 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/27859/stat): 27859 (minisat+_script) R 27858 27859 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784375807 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27859/statm): 174 3 169 147 0 27 0
[pid=27859] 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=27860
New process pid=27861
New process pid=27862
One traced child (pid=27861) exited with status: 0
execve syscall for /bin/sed executable
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=27862) exited with status: 0
One traced child (pid=27860) exited with status: 0
New process pid=27863
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-maros.opb

[startup+10.0033 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 27863
Raw data (/proc/27859/stat): 27859 (minisat+_script) S 27858 27859 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1784375807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27859/statm): 531 226 485 147 0 384 0
[pid=27859] vsize: 2124
Raw data (/proc/27863/stat): 27863 (minisat+_64-bit) R 27859 27859 27660 0 -1 0 481 0 0 0 989 2 0 0 25 0 1 0 1784375812 2297856 468 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27863/statm): 561 468 145 145 0 416 0
[pid=27863] vsize: 2244
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 4368

[startup+20.0051 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 27863
Raw data (/proc/27859/stat): 27859 (minisat+_script) S 27858 27859 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1784375807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27859/statm): 531 226 485 147 0 384 0
[pid=27859] vsize: 2124
Raw data (/proc/27863/stat): 27863 (minisat+_64-bit) R 27859 27859 27660 0 -1 0 523 0 0 0 1988 3 0 0 25 0 1 0 1784375812 2457600 510 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27863/statm): 600 510 145 145 0 455 0
[pid=27863] vsize: 2400
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 4524
One traced child (pid=27863) exited with status: 30
One traced child (pid=27859) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 23.4482
CPU time (s): 23.3694
CPU user time (s): 23.3065
CPU system time (s): 0.06299
CPU usage (%): 99.664
Max. virtual memory (cumulated for all children) (Kb): 4524

Verifier Data

Verifier:	OK	43097