PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-20-10-maros.opb
MD5SUM	df23206734a7a5ecc1a5d03632e7fa81
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	344750
Optimality of the best value was proved	NO
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 numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	29.6805
Number of variables	90
Total number of constraints	6
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	15
Maximum length of a constraint	90
Trace number 32111

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        924072 kB
Buffers:           520 kB
Cached:          89692 kB
SwapCached:        636 kB
Active:          14412 kB
Inactive:        77860 kB
HighTotal:      131008 kB
HighFree:        38584 kB
LowTotal:       903652 kB
LowFree:        885488 kB
SwapTotal:     2097892 kB
SwapFree:      2096396 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            12464 kB
Committed_AS:    63720 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 08:31:42 (client local time) WITH STATUS 30 IN 29.6805 SECONDS
stats: 23539 0 29.6805 30
#### END LAUNCHER DATA ####
#### BEGIN 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]---> BDD-cost: 1858
c ---[   2]---> BDD-cost:  357
c ---[   1]---> BDD-cost:  346
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6356    18148 |    2118       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 392806[0m
c ---[   0]---> Sorter-cost: 1272     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 |         0 |    9385    25223 |    3128       0        0     nan |  0.000 % |
c |       100 |    9385    25223 |    3440     100      723     7.2 |  0.970 % |
c ==============================================================================
c [1mFound solution: 376802[0m
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 |       239 |    9405    25314 |    3135     239     1642     6.9 |  0.970 % |
c |       339 |    9405    25314 |    3448     339     3701    10.9 |  0.994 % |
c |       489 |    9405    25314 |    3793     489     5187    10.6 |  0.994 % |
c ==============================================================================
c [1mFound solution: 375773[0m
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 |       548 |    9417    25350 |    3139     548     6609    12.1 |  0.994 % |
c |       649 |    9417    25350 |    3452     649     7749    11.9 |  1.020 % |
c |       800 |    9417    25350 |    3798     800     9633    12.0 |  1.020 % |
c |      1028 |    9417    25350 |    4178    1028    13601    13.2 |  1.020 % |
c ==============================================================================
c [1mFound solution: 374750[0m
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 |      1181 |    9428    25383 |    3142    1181    16931    14.3 |  1.020 % |
c |      1283 |    9428    25383 |    3456    1283    18013    14.0 |  1.046 % |
c ==============================================================================
c [1mFound solution: 368603[0m
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 |      1390 |    9435    25407 |    3145    1390    20650    14.9 |  1.046 % |
c |      1491 |    9435    25407 |    3459    1491    22170    14.9 |  1.072 % |
c |      1641 |    9435    25407 |    3805    1641    24324    14.8 |  1.072 % |
c |      1866 |    9435    25407 |    4185    1866    27512    14.7 |  1.072 % |
c |      2205 |    9435    25407 |    4604    2205    32414    14.7 |  1.072 % |
c ==============================================================================
c [1mFound solution: 366577[0m
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 |      2584 |    9451    25444 |    3150    2584    37701    14.6 |  1.072 % |
c |      2685 |    9451    25444 |    3465    2685    39793    14.8 |  1.098 % |
c |      2836 |    9451    25444 |    3811    2836    42370    14.9 |  1.098 % |
c ==============================================================================
c [1mFound solution: 366160[0m
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 |      3028 |    9470    25490 |    3156    3028    47637    15.7 |  1.098 % |
c |      3132 |    9470    25490 |    3471    3132    49312    15.7 |  1.122 % |
c |      3284 |    9470    25490 |    3818    3284    51298    15.6 |  1.123 % |
c |      3509 |    9470    25490 |    4200    3509    57619    16.4 |  1.122 % |
c |      3846 |    9470    25490 |    4620    3846    62795    16.3 |  1.122 % |
c ==============================================================================
c [1mFound solution: 364100[0m
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 |      3909 |    9486    25528 |    3162    3909    64642    16.5 |  1.122 % |
c |      4009 |    9486    25528 |    3478    2055    33763    16.4 |  1.148 % |
c |      4162 |    9486    25528 |    3826    2208    35879    16.2 |  1.148 % |
c |      4387 |    9486    25528 |    4208    2433    39242    16.1 |  1.148 % |
c |      4724 |    9486    25528 |    4629    2770    46814    16.9 |  1.148 % |
c |      5234 |    9486    25528 |    5092    3280    56071    17.1 |  1.148 % |
c ==============================================================================
c [1mFound solution: 358373[0m
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 |      5329 |    9502    25568 |    3167    3375    57819    17.1 |  1.148 % |
c |      5431 |    9502    25568 |    3483    1790    24912    13.9 |  1.173 % |
c |      5587 |    9502    25568 |    3832    1946    27073    13.9 |  1.173 % |
c |      5813 |    9502    25568 |    4215    2172    30148    13.9 |  1.173 % |
c |      6151 |    9502    25568 |    4636    2510    35104    14.0 |  1.173 % |
c ==============================================================================
c [1mFound solution: 350632[0m
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 |      6216 |    9518    25609 |    3172    2575    36197    14.1 |  1.173 % |
c |      6316 |    9518    25609 |    3489    2675    37568    14.0 |  1.198 % |
c ==============================================================================
c [1mFound solution: 350584[0m
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 |      6427 |    9535    25651 |    3178    2786    39204    14.1 |  1.198 % |
c ==============================================================================
c [1mFound solution: 349694[0m
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 |      6483 |    9551    25691 |    3183    2842    40484    14.2 |  1.198 % |
c |      6583 |    9551    25691 |    3501    2942    41739    14.2 |  1.246 % |
c |      6733 |    9551    25691 |    3851    3092    43619    14.1 |  1.246 % |
c |      6958 |    9551    25691 |    4236    3317    46742    14.1 |  1.246 % |
c |      7296 |    9551    25691 |    4660    3655    51268    14.0 |  1.246 % |
c |      7802 |    9551    25691 |    5126    4161    57655    13.9 |  1.246 % |
c ==============================================================================
c [1mFound solution: 347461[0m
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 |      8212 |    9568    25733 |    3189    4571    64519    14.1 |  1.246 % |
c |      8312 |    9568    25733 |    3507    2386    25935    10.9 |  1.269 % |
c |      8462 |    9568    25733 |    3858    2536    28084    11.1 |  1.269 % |
c |      8689 |    9568    25733 |    4244    2763    31098    11.3 |  1.269 % |
c |      9026 |    9568    25733 |    4669    3100    35590    11.5 |  1.269 % |
c |      9533 |    9568    25733 |    5135    3607    44107    12.2 |  1.269 % |
c |     10292 |    9568    25733 |    5649    4366    63935    14.6 |  1.269 % |
c |     11433 |    9568    25733 |    6214    5507    90916    16.5 |  1.269 % |
c ==============================================================================
c [1mFound solution: 347370[0m
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 |     12118 |    9586    25776 |    3195    6192   103898    16.8 |  1.269 % |
c |     12218 |    9586    25776 |    3514    3196    55056    17.2 |  1.293 % |
c |     12368 |    9586    25776 |    3865    3346    56516    16.9 |  1.294 % |
c |     12593 |    9586    25776 |    4252    3571    60989    17.1 |  1.294 % |
c |     12932 |    9586    25776 |    4677    3910    68065    17.4 |  1.293 % |
c |     13438 |    9586    25776 |    5145    4416    76048    17.2 |  1.294 % |
c ==============================================================================
c [1mFound solution: 347360[0m
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 |     13846 |    9598    25809 |    3199    4824    86061    17.8 |  1.294 % |
c |     13948 |    9598    25809 |    3518    2514    36825    14.6 |  1.318 % |
c |     14098 |    9598    25809 |    3870    2664    38797    14.6 |  1.318 % |
c |     14324 |    9598    25809 |    4257    2890    42774    14.8 |  1.318 % |
c |     14661 |    9598    25809 |    4683    3227    51026    15.8 |  1.318 % |
c |     15168 |    9598    25809 |    5152    3734    61390    16.4 |  1.318 % |
c ==============================================================================
c [1mFound solution: 347100[0m
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 |     15586 |    9611    25846 |    3203    4152    69805    16.8 |  1.318 % |
c |     15687 |    9611    25846 |    3523    2177    29676    13.6 |  1.342 % |
c ==============================================================================
c [1mFound solution: 347092[0m
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 |     15821 |    9624    25882 |    3208    2311    31337    13.6 |  1.342 % |
c |     15921 |    9624    25882 |    3528    2411    34667    14.4 |  1.366 % |
c |     16073 |    9624    25882 |    3881    2563    36360    14.2 |  1.366 % |
c |     16300 |    9624    25882 |    4269    2790    40012    14.3 |  1.366 % |
c |     16639 |    9624    25882 |    4696    3129    46488    14.9 |  1.366 % |
c |     17145 |    9624    25882 |    5166    3635    55703    15.3 |  1.366 % |
c |     17907 |    9624    25882 |    5683    4397    72357    16.5 |  1.366 % |
c ==============================================================================
c [1mFound solution: 347091[0m
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 |     17998 |    9635    25913 |    3211    4488    73740    16.4 |  1.366 % |
c |     18101 |    9635    25913 |    3532    2347    33812    14.4 |  1.390 % |
c |     18252 |    9635    25913 |    3885    2498    36295    14.5 |  1.390 % |
c ==============================================================================
c [1mFound solution: 347088[0m
c ---[   0]---> Sorter-cost:   11     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 |     18297 |    9646    25942 |    3215    2543    36883    14.5 |  1.390 % |
c |     18398 |    9646    25942 |    3536    2644    38589    14.6 |  1.414 % |
c |     18551 |    9646    25942 |    3890    2797    43784    15.7 |  1.414 % |
c |     18777 |    9646    25942 |    4279    3023    47866    15.8 |  1.414 % |
c |     19116 |    9646    25942 |    4707    3362    54312    16.2 |  1.414 % |
c ==============================================================================
c [1mFound solution: 346336[0m
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 |     19552 |    9656    25966 |    3218    3798    61666    16.2 |  1.414 % |
c |     19652 |    9656    25966 |    3539    1999    23762    11.9 |  1.438 % |
c |     19802 |    9656    25966 |    3893    2149    26115    12.2 |  1.439 % |
c |     20027 |    9656    25966 |    4283    2374    29441    12.4 |  1.438 % |
c |     20365 |    9656    25966 |    4711    2712    36728    13.5 |  1.438 % |
c |     20872 |    9656    25966 |    5182    3219    47164    14.7 |  1.438 % |
c ==============================================================================
c [1mFound solution: 345824[0m
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 |     21006 |    9667    25993 |    3222    3353    50283    15.0 |  1.438 % |
c |     21107 |    9667    25993 |    3544    1778    20545    11.6 |  1.463 % |
c |     21257 |    9667    25993 |    3898    1928    22733    11.8 |  1.463 % |
c |     21482 |    9667    25993 |    4288    2153    26829    12.5 |  1.463 % |
c |     21819 |    9667    25993 |    4717    2490    34487    13.9 |  1.463 % |
c |     22325 |    9667    25993 |    5189    2996    43091    14.4 |  1.463 % |
c |     23084 |    9667    25993 |    5707    3755    56274    15.0 |  1.463 % |
c ==============================================================================
c [1mFound solution: 345570[0m
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 |     23597 |    9679    26027 |    3226    4268    66445    15.6 |  1.463 % |
c |     23700 |    9679    26027 |    3548    2237    27022    12.1 |  1.486 % |
c |     23855 |    9672    26013 |    3903    2390    29041    12.2 |  1.566 % |
c |     24082 |    9672    26013 |    4293    2617    32231    12.3 |  1.566 % |
c |     24421 |    9672    26013 |    4723    2956    40330    13.6 |  1.566 % |
c |     24927 |    9672    26013 |    5195    3462    48424    14.0 |  1.566 % |
c ==============================================================================
c [1mFound solution: 345569[0m
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 |     25484 |    9684    26046 |    3228    4019    59689    14.9 |  1.566 % |
c |     25584 |    9684    26046 |    3550    2110    25640    12.2 |  1.590 % |
c |     25735 |    9684    26046 |    3905    2261    27607    12.2 |  1.590 % |
c |     25960 |    9684    26046 |    4296    2486    31170    12.5 |  1.589 % |
c |     26297 |    9684    26046 |    4726    2823    37935    13.4 |  1.589 % |
c ==============================================================================
c [1mFound solution: 345553[0m
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 |     26753 |    9698    26082 |    3232    3279    46756    14.3 |  1.589 % |
c |     26853 |    9698    26082 |    3555    3379    49103    14.5 |  1.613 % |
c |     27008 |    9698    26082 |    3910    3534    51461    14.6 |  1.613 % |
c |     27233 |    9698    26082 |    4301    3759    54460    14.5 |  1.612 % |
c |     27571 |    9698    26082 |    4731    4097    63117    15.4 |  1.612 % |
c |     28077 |    9698    26082 |    5205    4603    75277    16.4 |  1.613 % |
c ==============================================================================
c [1mFound solution: 345544[0m
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 |     28436 |    9712    26118 |    3237    4962    81506    16.4 |  1.613 % |
c |     28536 |    9712    26118 |    3560    2581    33986    13.2 |  1.636 % |
c |     28689 |    9712    26118 |    3916    2734    35967    13.2 |  1.636 % |
c |     28915 |    9712    26118 |    4308    2960    38339    13.0 |  1.636 % |
c |     29252 |    9712    26118 |    4739    3297    45884    13.9 |  1.636 % |
c ==============================================================================
c [1mFound solution: 345540[0m
c ---[   0]---> Sorter-cost:   11     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 |     29459 |    9724    26148 |    3241    3504    49203    14.0 |  1.636 % |
c |     29559 |    9724    26148 |    3565    1852    18697    10.1 |  1.659 % |
c ==============================================================================
c [1mFound solution: 345536[0m
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 |     29677 |    9739    26186 |    3246    1970    20520    10.4 |  1.659 % |
c ==============================================================================
c [1mFound solution: 345437[0m
c ---[   0]---> Sorter-cost:   11     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 |     29732 |    9754    26225 |    3251    2025    21895    10.8 |  1.659 % |
c ==============================================================================
c [1mFound solution: 345394[0m
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 |     29749 |    9773    26270 |    3257    2042    22259    10.9 |  1.659 % |
c |     29849 |    9773    26270 |    3582    2142    23811    11.1 |  1.725 % |
c |     30001 |    9773    26270 |    3940    2294    27524    12.0 |  1.725 % |
c |     30226 |    9773    26270 |    4335    2519    33341    13.2 |  1.725 % |
c |     30563 |    9773    26270 |    4768    2856    39825    13.9 |  1.725 % |
c |     31072 |    9773    26270 |    5245    3365    51243    15.2 |  1.725 % |
c |     31836 |    9773    26270 |    5769    4129    66290    16.1 |  1.725 % |
c ==============================================================================
c [1mFound solution: 345250[0m
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 |     32045 |    9789    26309 |    3263    4338    70046    16.1 |  1.725 % |
c |     32146 |    9789    26309 |    3589    2270    26947    11.9 |  1.747 % |
c |     32296 |    9789    26309 |    3948    2420    30388    12.6 |  1.747 % |
c |     32522 |    9789    26309 |    4343    2646    35116    13.3 |  1.747 % |
c |     32859 |    9789    26309 |    4777    2983    40750    13.7 |  1.747 % |
c |     33367 |    9789    26309 |    5255    3491    49414    14.2 |  1.747 % |
c |     34127 |    9789    26309 |    5780    4251    61693    14.5 |  1.747 % |
c ==============================================================================
c [1mFound solution: 345248[0m
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 |     34416 |    9805    26347 |    3268    4540    66080    14.6 |  1.747 % |
c |     34516 |    9805    26347 |    3594    2370    25439    10.7 |  1.769 % |
c ==============================================================================
c [1mFound solution: 345246[0m
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 |     34639 |    9821    26385 |    3273    2493    27645    11.1 |  1.769 % |
c ==============================================================================
c [1mFound solution: 345244[0m
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 |     34708 |    9837    26425 |    3279    2562    29056    11.3 |  1.769 % |
c |     34808 |    9837    26425 |    3606    2662    31192    11.7 |  1.812 % |
c |     34961 |    9837    26425 |    3967    2815    33134    11.8 |  1.813 % |
c |     35186 |    9837    26425 |    4364    3040    35901    11.8 |  1.812 % |
c |     35523 |    9837    26425 |    4800    3377    44571    13.2 |  1.812 % |
c ==============================================================================
c [1mFound solution: 345240[0m
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 |     35642 |    9853    26463 |    3284    3496    46344    13.3 |  1.812 % |
c |     35742 |    9853    26463 |    3612    1848    18997    10.3 |  1.834 % |
c |     35892 |    9853    26463 |    3973    1998    20811    10.4 |  1.835 % |
c ==============================================================================
c [1mFound solution: 345238[0m
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 |     35931 |    9871    26506 |    3290    2037    21465    10.5 |  1.835 % |
c ==============================================================================
c [1mFound solution: 345237[0m
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 |     35933 |    9889    26549 |    3296    2039    21493    10.5 |  1.835 % |
c ==============================================================================
c [1mFound solution: 344981[0m
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 |     36009 |    9899    26574 |    3299    2115    23364    11.0 |  1.835 % |
c |     36110 |    9899    26574 |    3628    2216    24868    11.2 |  1.900 % |
c |     36260 |    9899    26574 |    3991    2366    27287    11.5 |  1.899 % |
c |     36486 |    9899    26574 |    4390    2592    31268    12.1 |  1.899 % |
c |     36824 |    9899    26574 |    4830    2930    39804    13.6 |  1.899 % |
c ==============================================================================
c [1mFound solution: 344980[0m
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 |     37160 |    9912    26608 |    3304    3266    43585    13.3 |  1.899 % |
c |     37262 |    9912    26608 |    3634    3368    45679    13.6 |  1.922 % |
c |     37412 |    9912    26608 |    3997    3518    50107    14.2 |  1.921 % |
c ==============================================================================
c [1mFound solution: 344978[0m
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 |     37581 |    9927    26645 |    3309    3687    53286    14.5 |  1.921 % |
c |     37681 |    9927    26645 |    3639    1944    21735    11.2 |  1.943 % |
c |     37831 |    9927    26645 |    4003    2094    24716    11.8 |  1.944 % |
c |     38056 |    9927    26645 |    4404    2319    30074    13.0 |  1.943 % |
c |     38395 |    9927    26645 |    4844    2658    35782    13.5 |  1.943 % |
c ==============================================================================
c [1mFound solution: 344928[0m
c ---[   0]---> Sorter-cost:   11     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 |     38435 |    9940    26677 |    3313    2698    36301    13.5 |  1.943 % |
c ==============================================================================
c [1mFound solution: 344927[0m
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 |     38486 |    9953    26712 |    3317    2749    36920    13.4 |  1.943 % |
c ==============================================================================
c [1mFound solution: 344925[0m
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 |     38511 |    9963    26736 |    3321    2774    37496    13.5 |  1.943 % |
c |     38612 |    9963    26736 |    3653    2875    39184    13.6 |  2.011 % |
c ==============================================================================
c [1mFound solution: 344920[0m
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 |     38662 |    9976    26768 |    3325    2925    40531    13.9 |  2.011 % |
c |     38762 |    9976    26768 |    3657    3025    42310    14.0 |  2.032 % |
c |     38912 |    9976    26768 |    4023    3175    46836    14.8 |  2.032 % |
c ==============================================================================
c [1mFound solution: 344901[0m
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 |     39047 |    9986    26792 |    3328    3310    49622    15.0 |  2.032 % |
c |     39151 |    9986    26792 |    3660    3414    52592    15.4 |  2.054 % |
c |     39301 |    9986    26792 |    4026    3564    54855    15.4 |  2.054 % |
c |     39526 |    9986    26792 |    4429    3789    58600    15.5 |  2.054 % |
c |     39864 |    9986    26792 |    4872    4127    63785    15.5 |  2.055 % |
c |     40371 |    9986    26792 |    5359    4634    72963    15.7 |  2.054 % |
c ==============================================================================
c [1mFound solution: 344900[0m
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 |     40868 |    9998    26821 |    3332    5131    81558    15.9 |  2.054 % |
c |     40969 |    9998    26821 |    3665    2667    34527    12.9 |  2.077 % |
c |     41119 |    9998    26821 |    4031    2817    36409    12.9 |  2.077 % |
c |     41344 |    9998    26821 |    4434    3042    39649    13.0 |  2.078 % |
c |     41681 |    9998    26821 |    4878    3379    45249    13.4 |  2.077 % |
c ==============================================================================
c [1mFound solution: 344835[0m
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 |     41782 |   10011    26852 |    3337    3480    46537    13.4 |  2.077 % |
c |     41882 |   10011    26852 |    3670    1840    17757     9.7 |  2.099 % |
c |     42032 |   10011    26852 |    4037    1990    20246    10.2 |  2.099 % |
c ==============================================================================
c [1mFound solution: 344832[0m
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 |     42110 |   10024    26883 |    3341    2068    21625    10.5 |  2.099 % |
c |     42214 |   10024    26883 |    3675    2172    24483    11.3 |  2.121 % |
c |     42364 |   10024    26883 |    4042    2322    27924    12.0 |  2.122 % |
c |     42590 |   10024    26883 |    4446    2548    31818    12.5 |  2.121 % |
c |     42928 |    9804    26363 |    4891    2577    33392    13.0 |  3.661 % |
c |     43435 |    9676    26034 |    5380    3004    40987    13.6 |  4.494 % |
c |     44194 |    9676    26034 |    5918    3763    53296    14.2 |  4.494 % |
c |     45334 |    9676    26034 |    6510    4903    82102    16.7 |  4.494 % |
c ==============================================================================
c [1mFound solution: 344831[0m
c ---[   0]---> Sorter-cost:  310     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 |     45413 |   10307    27502 |    3435    4978    84048    16.9 |  4.494 % |
c ==============================================================================
c [1mFound solution: 344827[0m
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 |     45447 |   10324    27543 |    3441    2523    36283    14.4 |  4.494 % |
c |     45547 |   10324    27543 |    3785    2623    38002    14.5 |  4.409 % |
c |     45698 |   10324    27543 |    4163    2774    41386    14.9 |  4.409 % |
c |     45923 |   10324    27543 |    4579    2999    45453    15.2 |  4.409 % |
c ==============================================================================
c [1mFound solution: 344801[0m
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 |     46129 |   10338    27578 |    3446    3205    50527    15.8 |  4.409 % |
c |     46229 |   10338    27578 |    3790    3305    54250    16.4 |  4.425 % |
c ==============================================================================
c [1mFound solution: 344798[0m
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 |     46370 |   10352    27611 |    3450    3446    56743    16.5 |  4.425 % |
c |     46471 |   10352    27611 |    3795    3547    59819    16.9 |  4.441 % |
c |     46622 |   10352    27611 |    4174    3698    63979    17.3 |  4.441 % |
c |     46848 |   10352    27611 |    4591    3924    68576    17.5 |  4.442 % |
c ==============================================================================
c [1mFound solution: 344796[0m
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 |     46922 |   10366    27644 |    3455    3998    69616    17.4 |  4.442 % |
c |     47022 |   10366    27644 |    3800    2099    27329    13.0 |  4.458 % |
c |     47173 |   10366    27644 |    4180    2250    29141    13.0 |  4.458 % |
c ==============================================================================
c [1mFound solution: 344793[0m
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 |     47360 |   10383    27686 |    3461    2437    32757    13.4 |  4.458 % |
c |     47460 |   10383    27686 |    3807    2537    34924    13.8 |  4.472 % |
c |     47610 |   10383    27686 |    4187    2687    37174    13.8 |  4.472 % |
c ==============================================================================
c [1mFound solution: 344792[0m
c ---[   0]---> Sorter-cost:   11     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 |     47705 |   10397    27718 |    3465    2782    40021    14.4 |  4.472 % |
c |     47805 |   10397    27718 |    3811    2882    41758    14.5 |  4.488 % |
c ==============================================================================
c [1mFound solution: 344791[0m
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 |     47822 |   10413    27757 |    3471    2899    41960    14.5 |  4.488 % |
c |     47922 |   10413    27757 |    3818    2999    44279    14.8 |  4.503 % |
c ==============================================================================
c [1mFound solution: 344765[0m
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 |     47988 |   10430    27798 |    3476    3065    46035    15.0 |  4.503 % |
c |     48088 |   10430    27798 |    3823    3165    47233    14.9 |  4.517 % |
c |     48238 |   10430    27798 |    4205    3315    50301    15.2 |  4.517 % |
c |     48464 |   10430    27798 |    4626    3541    55183    15.6 |  4.517 % |
c |     48801 |   10430    27798 |    5089    3878    63695    16.4 |  4.517 % |
c |     49308 |   10430    27798 |    5598    4385    72993    16.6 |  4.517 % |
c ==============================================================================
c [1mFound solution: 344764[0m
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 |     49837 |   10437    27819 |    3479    4908    81000    16.5 |  4.517 % |
c |     49937 |   10437    27819 |    3826    2554    30653    12.0 |  4.624 % |
c ==============================================================================
c [1mFound solution: 344763[0m
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 |     50020 |   10453    27856 |    3484    2637    32006    12.1 |  4.624 % |
c |     50122 |   10453    27856 |    3832    2739    34623    12.6 |  4.639 % |
c |     50272 |   10453    27856 |    4215    2889    36823    12.7 |  4.639 % |
c |     50498 |   10453    27856 |    4637    3115    41806    13.4 |  4.639 % |
c |     50835 |   10453    27856 |    5100    3452    50169    14.5 |  4.639 % |
c ==============================================================================
c [1mFound solution: 344760[0m
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 |     50846 |   10469    27893 |    3489    3463    50350    14.5 |  4.639 % |
c ==============================================================================
c [1mFound solution: 344754[0m
c ---[   0]---> Sorter-cost:   11     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 |     50847 |   10483    27925 |    3494    3464    50358    14.5 |  4.639 % |
c ==============================================================================
c [1mFound solution: 344753[0m
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 |     50863 |   10499    27962 |    3499    3480    50675    14.6 |  4.639 % |
c |     50963 |   10499    27962 |    3848    3580    53216    14.9 |  4.684 % |
c ==============================================================================
c [1mFound solution: 344751[0m
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 |     50972 |   10517    28004 |    3505    3589    53282    14.8 |  4.684 % |
c ==============================================================================
c [1mFound solution: 344750[0m
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 |     50975 |   10535    28046 |    3511    3592    53329    14.8 |  4.684 % |
c |     51075 |   10535    28046 |    3862    3692    55729    15.1 |  4.711 % |
c |     51227 |   10535    28046 |    4248    3844    58650    15.3 |  4.710 % |
c |     51453 |   10535    28046 |    4673    4070    63649    15.6 |  4.710 % |
c |     51791 |   10535    28046 |    5140    4408    69944    15.9 |  4.712 % |
c |     52298 |   10535    28046 |    5654    4915    79145    16.1 |  4.711 % |
c |     53057 |   10535    28046 |    6219    5674    93027    16.4 |  4.710 % |
c ==============================================================================
c [1mOptimal solution: 344750[0m
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              : 236
c conflicts             : 53458          (1805 /sec)
c decisions             : 120698         (4076 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 29.6155 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.88 0.95 0.91 2/54 17227
Raw data (stat): 17227 (runsolver) R 17226 20687 20686 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854745934 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.90 0.95 0.91 2/55 17231
Raw data (stat): 17227 (minisat+_script) S 17226 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854745934 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 17231
Raw data (stat): 17227 (minisat+_script) S 17226 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854745934 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+29.6964 s]
Raw data (loadavg): 0.93 0.96 0.91 1/53 17231
Raw data (stat): 17227 (minisat+_script) S 17226 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854745934 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 29.6958
CPU time (s): 29.6805
CPU user time (s): 29.6235
CPU system time (s): 0.056991
CPU usage (%): 99.9484
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	344750
#### END VERIFIER DATA ####