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-13-7/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-13-7-maros.opb
MD5SUM	1ae5b04b2d0e1f5ab82e29e98b8350c0
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	43097
Optimality of the best value was proved	NO
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 numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02384
Number of variables	64
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	12
Maximum length of a constraint	64
Trace number 14082

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-20 23:10:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20384 boxname=wulflinc5 idbench=1568 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1ae5b04b2d0e1f5ab82e29e98b8350c0  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-maros.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-maros.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-maros.opb
IDLAUNCH: 20384
/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:        574216 kB
Buffers:         39100 kB
Cached:         396548 kB
SwapCached:       2272 kB
Active:         219568 kB
Inactive:       221232 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        573964 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14052 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:10:42 (client local time) WITH STATUS 30 IN 26.212 SECONDS
stats: 20384 0 26.212 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:   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 |    4875    11531 |    1625       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 52686[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  989     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 |        10 |    7484    17691 |    2494      10      155    15.5 |  0.000 % |
c |       110 |    7484    17691 |    2743     110     2029    18.4 |  0.976 % |
c ==============================================================================
c [1mFound solution: 52195[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       111 |    7524    17797 |    2508     111     2033    18.3 |  0.976 % |
c ==============================================================================
c [1mFound solution: 50147[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       159 |    7534    17821 |    2511     159     3117    19.6 |  0.976 % |
c |       259 |    7534    17821 |    2762     259     4242    16.4 |  1.052 % |
c ==============================================================================
c [1mFound solution: 48102[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |       267 |    7585    17958 |    2528     267     4284    16.0 |  1.052 % |
c ==============================================================================
c [1mFound solution: 47130[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |       272 |    7610    18021 |    2536     272     4324    15.9 |  1.052 % |
c ==============================================================================
c [1mFound solution: 47058[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |       274 |    7630    18073 |    2543     274     4370    15.9 |  1.052 % |
c ==============================================================================
c [1mFound solution: 47014[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       278 |    7648    18121 |    2549     278     4457    16.0 |  1.052 % |
c |       378 |    7648    18121 |    2803     378     5383    14.2 |  1.202 % |
c |       528 |    7648    18121 |    3084     528     7278    13.8 |  1.202 % |
c ==============================================================================
c [1mFound solution: 46534[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       685 |    7670    18177 |    2556     685    11303    16.5 |  1.202 % |
c |       786 |    7670    18177 |    2811     786    13444    17.1 |  1.240 % |
c |       939 |    7670    18177 |    3092     939    15979    17.0 |  1.239 % |
c |      1164 |    7670    18177 |    3402    1164    20217    17.4 |  1.239 % |
c |      1502 |    7670    18177 |    3742    1502    25452    16.9 |  1.239 % |
c ==============================================================================
c [1mFound solution: 46498[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1810 |    7693    18234 |    2564    1810    32068    17.7 |  1.239 % |
c ==============================================================================
c [1mFound solution: 46496[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |      1831 |    7724    18311 |    2574    1831    32429    17.7 |  1.239 % |
c ==============================================================================
c [1mFound solution: 46306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1900 |    7741    18354 |    2580    1900    33728    17.8 |  1.239 % |
c |      2001 |    7741    18354 |    2838    2001    36179    18.1 |  1.348 % |
c |      2151 |    7741    18354 |    3121    2151    38944    18.1 |  1.348 % |
c |      2376 |    7741    18354 |    3433    2376    42406    17.8 |  1.348 % |
c ==============================================================================
c [1mFound solution: 46032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2432 |    7762    18409 |    2587    2432    43983    18.1 |  1.348 % |
c |      2533 |    7762    18409 |    2845    2533    45264    17.9 |  1.385 % |
c |      2684 |    7762    18409 |    3130    2684    47281    17.6 |  1.385 % |
c |      2910 |    7762    18409 |    3443    2910    50166    17.2 |  1.385 % |
c ==============================================================================
c [1mFound solution: 44401[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |      3020 |    7794    18489 |    2598    3020    52263    17.3 |  1.385 % |
c |      3121 |    7778    18446 |    2857    1606    21762    13.6 |  1.459 % |
c |      3272 |    7778    18446 |    3143    1757    24467    13.9 |  1.458 % |
c ==============================================================================
c [1mFound solution: 44253[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |      3477 |    7800    18502 |    2600    1962    29116    14.8 |  1.458 % |
c |      3577 |    7800    18502 |    2860    2062    30799    14.9 |  1.495 % |
c |      3728 |    7800    18502 |    3146    2213    34881    15.8 |  1.494 % |
c |      3955 |    7800    18502 |    3460    2440    38465    15.8 |  1.495 % |
c |      4292 |    7800    18502 |    3806    2777    43838    15.8 |  1.495 % |
c |      4798 |    7800    18502 |    4187    3283    53097    16.2 |  1.495 % |
c |      5557 |    7800    18502 |    4606    4042    64714    16.0 |  1.495 % |
c |      6696 |    7800    18502 |    5066    2750    34671    12.6 |  1.495 % |
c ==============================================================================
c [1mFound solution: 44250[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6868 |    7816    18542 |    2605    2922    37817    12.9 |  1.495 % |
c ==============================================================================
c [1mFound solution: 43572[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |      6925 |    7846    18614 |    2615    1518    17274    11.4 |  1.495 % |
c |      7025 |    7846    18614 |    2876    1618    18939    11.7 |  1.564 % |
c |      7175 |    7846    18614 |    3164    1768    21732    12.3 |  1.564 % |
c |      7400 |    7846    18614 |    3480    1993    25992    13.0 |  1.564 % |
c |      7739 |    7846    18614 |    3828    2332    33251    14.3 |  1.564 % |
c |      8245 |    7846    18614 |    4211    2838    43956    15.5 |  1.564 % |
c |      9004 |    7846    18614 |    4632    3597    56452    15.7 |  1.564 % |
c ==============================================================================
c [1mFound solution: 43488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9485 |    7862    18654 |    2620    4078    66704    16.4 |  1.564 % |
c |      9586 |    7862    18654 |    2882    2140    28477    13.3 |  1.600 % |
c |      9737 |    7862    18654 |    3170    2291    31394    13.7 |  1.600 % |
c ==============================================================================
c [1mFound solution: 43485[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9817 |    7876    18688 |    2625    2371    33126    14.0 |  1.600 % |
c |      9918 |    7876    18688 |    2887    2472    34686    14.0 |  1.636 % |
c |     10069 |    7876    18688 |    3176    2623    36698    14.0 |  1.636 % |
c |     10294 |    7876    18688 |    3493    2848    42315    14.9 |  1.636 % |
c |     10631 |    7876    18688 |    3843    3185    47886    15.0 |  1.636 % |
c |     11137 |    7876    18688 |    4227    3691    56700    15.4 |  1.636 % |
c ==============================================================================
c [1mFound solution: 43430[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11763 |    7892    18728 |    2630    4317    69340    16.1 |  1.636 % |
c |     11863 |    7892    18728 |    2893    2259    29812    13.2 |  1.672 % |
c |     12014 |    7892    18728 |    3182    2410    33264    13.8 |  1.671 % |
c |     12239 |    7892    18728 |    3500    2635    38394    14.6 |  1.672 % |
c |     12576 |    7892    18728 |    3850    2972    43354    14.6 |  1.672 % |
c |     13082 |    7892    18728 |    4235    3478    53740    15.5 |  1.672 % |
c ==============================================================================
c [1mFound solution: 43407[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     13323 |    7919    18793 |    2639    3719    57745    15.5 |  1.672 % |
c |     13423 |    7919    18793 |    2902    1960    23242    11.9 |  1.704 % |
c |     13573 |    7919    18793 |    3193    2110    25824    12.2 |  1.704 % |
c |     13798 |    7919    18793 |    3512    2335    29946    12.8 |  1.704 % |
c |     14135 |    7919    18793 |    3863    2672    35888    13.4 |  1.704 % |
c |     14645 |    7919    18793 |    4250    3182    45178    14.2 |  1.704 % |
c |     15409 |    7919    18793 |    4675    3946    61899    15.7 |  1.704 % |
c ==============================================================================
c [1mFound solution: 43402[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16389 |    7943    18851 |    2647    4926    79147    16.1 |  1.704 % |
c |     16490 |    7943    18851 |    2911    2564    32354    12.6 |  1.739 % |
c |     16640 |    7943    18851 |    3202    2714    34147    12.6 |  1.738 % |
c |     16866 |    7943    18851 |    3523    2940    38711    13.2 |  1.738 % |
c ==============================================================================
c [1mFound solution: 43401[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     16976 |    7971    18919 |    2657    3050    40924    13.4 |  1.738 % |
c |     17078 |    7971    18919 |    2922    1627    16787    10.3 |  1.770 % |
c |     17230 |    7971    18919 |    3214    1779    19507    11.0 |  1.770 % |
c |     17455 |    7971    18919 |    3536    2004    23262    11.6 |  1.770 % |
c |     17793 |    7971    18919 |    3890    2342    29432    12.6 |  1.770 % |
c |     18301 |    7971    18919 |    4279    2850    41606    14.6 |  1.770 % |
c |     19064 |    7971    18919 |    4707    3613    56523    15.6 |  1.770 % |
c ==============================================================================
c [1mFound solution: 43400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     19188 |    7999    18987 |    2666    3737    58712    15.7 |  1.770 % |
c |     19288 |    7999    18987 |    2932    1969    24256    12.3 |  1.802 % |
c |     19439 |    7999    18987 |    3225    2120    26571    12.5 |  1.802 % |
c |     19664 |    7999    18987 |    3548    2345    31250    13.3 |  1.802 % |
c ==============================================================================
c [1mFound solution: 43396[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19786 |    8023    19045 |    2674    2467    33182    13.5 |  1.802 % |
c |     19889 |    8023    19045 |    2941    2570    35093    13.7 |  1.835 % |
c |     20039 |    8023    19045 |    3235    2720    38496    14.2 |  1.835 % |
c |     20265 |    8023    19045 |    3559    2946    41979    14.2 |  1.835 % |
c ==============================================================================
c [1mFound solution: 43395[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20561 |    8041    19089 |    2680    3242    48805    15.1 |  1.835 % |
c |     20662 |    8041    19089 |    2948    1722    19553    11.4 |  1.869 % |
c |     20812 |    8041    19089 |    3242    1872    21856    11.7 |  1.869 % |
c |     21037 |    8041    19089 |    3567    2097    25126    12.0 |  1.869 % |
c |     21374 |    8041    19089 |    3923    2434    31907    13.1 |  1.869 % |
c ==============================================================================
c [1mFound solution: 43394[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21824 |    8063    19143 |    2687    2884    40737    14.1 |  1.869 % |
c |     21925 |    8063    19143 |    2955    1543    15882    10.3 |  1.902 % |
c |     22076 |    8063    19143 |    3251    1694    18149    10.7 |  1.902 % |
c |     22301 |    8063    19143 |    3576    1919    21793    11.4 |  1.902 % |
c |     22640 |    8063    19143 |    3934    2258    28195    12.5 |  1.902 % |
c |     23146 |    8063    19143 |    4327    2764    38456    13.9 |  1.902 % |
c ==============================================================================
c [1mFound solution: 43393[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23511 |    8085    19197 |    2695    3129    43390    13.9 |  1.902 % |
c |     23613 |    8085    19197 |    2964    1667    16099     9.7 |  1.935 % |
c |     23763 |    8085    19197 |    3260    1817    18692    10.3 |  1.935 % |
c |     23991 |    8085    19197 |    3587    2045    21960    10.7 |  1.935 % |
c |     24331 |    8085    19197 |    3945    2385    28629    12.0 |  1.935 % |
c |     24839 |    8085    19197 |    4340    2893    37738    13.0 |  1.935 % |
c ==============================================================================
c [1mFound solution: 43392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25280 |    8107    19251 |    2702    3334    44522    13.4 |  1.935 % |
c |     25380 |    8107    19251 |    2972    1767    17787    10.1 |  1.968 % |
c |     25531 |    8107    19251 |    3269    1918    19893    10.4 |  1.968 % |
c |     25756 |    8107    19251 |    3596    2143    25237    11.8 |  1.968 % |
c |     26094 |    8107    19251 |    3955    2481    31955    12.9 |  1.968 % |
c |     26601 |    8107    19251 |    4351    2988    42628    14.3 |  1.968 % |
c ==============================================================================
c [1mFound solution: 43376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26689 |    8126    19298 |    2708    3076    43905    14.3 |  1.968 % |
c |     26790 |    8126    19298 |    2978    1639    16227     9.9 |  2.001 % |
c ==============================================================================
c [1mFound solution: 43362[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26908 |    8146    19346 |    2715    1757    18534    10.5 |  2.001 % |
c |     27009 |    8146    19346 |    2986    1858    20345    10.9 |  2.033 % |
c |     27160 |    8146    19346 |    3285    2009    22906    11.4 |  2.033 % |
c |     27385 |    8146    19346 |    3613    2234    27462    12.3 |  2.033 % |
c |     27724 |    8146    19346 |    3975    2573    33325    13.0 |  2.033 % |
c |     28231 |    8146    19346 |    4372    3080    42922    13.9 |  2.033 % |
c ==============================================================================
c [1mFound solution: 43332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28314 |    8166    19394 |    2722    3163    44463    14.1 |  2.033 % |
c |     28415 |    8166    19394 |    2994    1683    17519    10.4 |  2.066 % |
c |     28565 |    8166    19394 |    3293    1833    19606    10.7 |  2.065 % |
c |     28791 |    8166    19394 |    3622    2059    24992    12.1 |  2.066 % |
c ==============================================================================
c [1mFound solution: 43331[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28903 |    8186    19442 |    2728    2171    26933    12.4 |  2.066 % |
c |     29003 |    8186    19442 |    3000    2271    29051    12.8 |  2.098 % |
c ==============================================================================
c [1mFound solution: 43328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29044 |    8209    19497 |    2736    2312    29609    12.8 |  2.098 % |
c ==============================================================================
c [1mFound solution: 43325[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29074 |    8236    19562 |    2745    2342    30018    12.8 |  2.098 % |
c |     29174 |    8236    19562 |    3019    2442    31760    13.0 |  2.160 % |
c ==============================================================================
c [1mFound solution: 43322[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29208 |    8262    19624 |    2754    2476    32301    13.0 |  2.160 % |
c |     29308 |    8262    19624 |    3029    2576    33985    13.2 |  2.189 % |
c |     29458 |    8262    19624 |    3332    2726    36549    13.4 |  2.188 % |
c |     29685 |    8262    19624 |    3665    2953    40010    13.5 |  2.189 % |
c |     30024 |    8262    19624 |    4032    3292    49004    14.9 |  2.189 % |
c ==============================================================================
c [1mFound solution: 43320[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30184 |    8291    19693 |    2763    3452    52338    15.2 |  2.189 % |
c |     30284 |    8291    19693 |    3039    1826    20605    11.3 |  2.218 % |
c |     30438 |    8291    19693 |    3343    1980    22338    11.3 |  2.221 % |
c |     30663 |    8291    19693 |    3677    2205    27494    12.5 |  2.217 % |
c ==============================================================================
c [1mFound solution: 43316[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30811 |    8308    19734 |    2769    2353    29453    12.5 |  2.217 % |
c |     30914 |    8308    19734 |    3045    2456    31329    12.8 |  2.249 % |
c |     31065 |    8308    19734 |    3350    2607    33624    12.9 |  2.253 % |
c ==============================================================================
c [1mFound solution: 43314[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31087 |    8331    19789 |    2777    2629    34060    13.0 |  2.253 % |
c ==============================================================================
c [1mFound solution: 43306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31110 |    8354    19844 |    2784    2652    34580    13.0 |  2.253 % |
c |     31210 |    8354    19844 |    3062    2752    36896    13.4 |  2.309 % |
c |     31360 |    8354    19844 |    3368    2902    39023    13.4 |  2.313 % |
c |     31586 |    8354    19844 |    3705    3128    45434    14.5 |  2.310 % |
c |     31924 |    8354    19844 |    4076    3466    52927    15.3 |  2.310 % |
c ==============================================================================
c [1mFound solution: 43295[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32101 |    8376    19898 |    2792    3643    55897    15.3 |  2.310 % |
c ==============================================================================
c [1mFound solution: 43294[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32193 |    8398    19952 |    2799    1914    21297    11.1 |  2.310 % |
c |     32293 |    8398    19952 |    3078    2014    23813    11.8 |  2.372 % |
c |     32444 |    8398    19952 |    3386    2165    27372    12.6 |  2.371 % |
c ==============================================================================
c [1mFound solution: 43255[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     32545 |    8423    20013 |    2807    2266    29469    13.0 |  2.371 % |
c |     32645 |    8423    20013 |    3087    2366    31146    13.2 |  2.400 % |
c |     32795 |    8423    20013 |    3396    2516    35786    14.2 |  2.400 % |
c |     33020 |    8423    20013 |    3736    2741    41611    15.2 |  2.400 % |
c |     33358 |    8423    20013 |    4109    3079    50391    16.4 |  2.400 % |
c |     33867 |    8423    20013 |    4520    3588    60231    16.8 |  2.400 % |
c ==============================================================================
c [1mFound solution: 43254[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34043 |    8448    20074 |    2816    3764    63683    16.9 |  2.400 % |
c |     34145 |    8448    20074 |    3097    1984    22402    11.3 |  2.431 % |
c |     34295 |    8448    20074 |    3407    2134    24451    11.5 |  2.430 % |
c |     34520 |    8448    20074 |    3748    2359    28557    12.1 |  2.430 % |
c ==============================================================================
c [1mFound solution: 43246[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34561 |    8467    20121 |    2822    2400    29340    12.2 |  2.430 % |
c |     34661 |    8467    20121 |    3104    2500    31301    12.5 |  2.460 % |
c |     34811 |    8467    20121 |    3414    2650    33691    12.7 |  2.460 % |
c |     35036 |    8467    20121 |    3756    2875    37318    13.0 |  2.460 % |
c ==============================================================================
c [1mFound solution: 43238[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35131 |    8485    20165 |    2828    2970    39140    13.2 |  2.460 % |
c |     35231 |    8485    20165 |    3110    1585    15901    10.0 |  2.491 % |
c |     35381 |    8485    20165 |    3421    1735    18156    10.5 |  2.491 % |
c |     35606 |    8485    20165 |    3764    1960    22850    11.7 |  2.491 % |
c |     35945 |    8485    20165 |    4140    2299    29465    12.8 |  2.495 % |
c ==============================================================================
c [1mFound solution: 43221[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     36097 |    8506    20218 |    2835    2451    31920    13.0 |  2.495 % |
c ==============================================================================
c [1mFound solution: 43215[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36146 |    8522    20258 |    2840    2500    32694    13.1 |  2.495 % |
c ==============================================================================
c [1mFound solution: 43181[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36238 |    8545    20315 |    2848    2592    34369    13.3 |  2.495 % |
c ==============================================================================
c [1mFound solution: 43176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36240 |    8564    20362 |    2854    2594    34394    13.3 |  2.495 % |
c ==============================================================================
c [1mFound solution: 43174[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36260 |    8580    20402 |    2860    2614    34718    13.3 |  2.495 % |
c |     36360 |    8580    20402 |    3146    2714    36723    13.5 |  2.644 % |
c |     36510 |    8580    20402 |    3460    2864    39238    13.7 |  2.644 % |
c |     36735 |    8580    20402 |    3806    3089    43276    14.0 |  2.644 % |
c |     37072 |    8580    20402 |    4187    3426    49915    14.6 |  2.644 % |
c |     37579 |    8580    20402 |    4606    3933    59988    15.3 |  2.644 % |
c ==============================================================================
c [1mFound solution: 43166[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37810 |    8598    20446 |    2866    4164    65673    15.8 |  2.644 % |
c |     37910 |    8598    20446 |    3152    2182    26813    12.3 |  2.674 % |
c |     38060 |    8598    20446 |    3467    2332    28692    12.3 |  2.674 % |
c |     38287 |    8598    20446 |    3814    2559    33020    12.9 |  2.674 % |
c |     38624 |    8598    20446 |    4196    2896    40899    14.1 |  2.674 % |
c ==============================================================================
c [1mFound solution: 43165[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38691 |    8619    20497 |    2873    2963    42126    14.2 |  2.674 % |
c |     38792 |    8619    20497 |    3160    1583    14330     9.1 |  2.703 % |
c ==============================================================================
c [1mFound solution: 43163[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38872 |    8641    20551 |    2880    1663    15690     9.4 |  2.703 % |
c |     38973 |    8641    20551 |    3168    1764    17390     9.9 |  2.732 % |
c |     39123 |    8641    20551 |    3484    1914    19825    10.4 |  2.732 % |
c |     39350 |    8641    20551 |    3833    2141    23491    11.0 |  2.731 % |
c ==============================================================================
c [1mFound solution: 43159[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39494 |    8662    20602 |    2887    2285    25517    11.2 |  2.731 % |
c |     39594 |    8662    20602 |    3175    2385    27363    11.5 |  2.760 % |
c ==============================================================================
c [1mFound solution: 43154[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39665 |    8683    20653 |    2894    2456    28889    11.8 |  2.760 % |
c |     39766 |    8683    20653 |    3183    2557    30397    11.9 |  2.789 % |
c |     39920 |    8683    20653 |    3501    2711    33558    12.4 |  2.789 % |
c |     40147 |    8683    20653 |    3851    2938    36722    12.5 |  2.789 % |
c ==============================================================================
c [1mFound solution: 43130[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40269 |    8701    20697 |    2900    3060    38892    12.7 |  2.789 % |
c ==============================================================================
c [1mFound solution: 43126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40362 |    8720    20744 |    2906    1623    14633     9.0 |  2.789 % |
c |     40462 |    8720    20744 |    3196    1723    16916     9.8 |  2.847 % |
c |     40612 |    8720    20744 |    3516    1873    18913    10.1 |  2.847 % |
c |     40837 |    8720    20744 |    3867    2098    22591    10.8 |  2.847 % |
c ==============================================================================
c [1mFound solution: 43125[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41123 |    8742    20798 |    2914    2384    26369    11.1 |  2.847 % |
c |     41223 |    8742    20798 |    3205    2484    28491    11.5 |  2.875 % |
c |     41374 |    8742    20798 |    3525    2635    31859    12.1 |  2.876 % |
c |     41599 |    8742    20798 |    3878    2860    35889    12.5 |  2.875 % |
c ==============================================================================
c [1mFound solution: 43123[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41654 |    8761    20845 |    2920    2915    37380    12.8 |  2.875 % |
c |     41755 |    8761    20845 |    3212    3016    39361    13.1 |  2.904 % |
c |     41905 |    8761    20845 |    3533    3166    41482    13.1 |  2.904 % |
c ==============================================================================
c [1mFound solution: 43120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42074 |    8776    20882 |    2925    3335    43929    13.2 |  2.904 % |
c |     42175 |    8776    20882 |    3217    1769    15887     9.0 |  2.934 % |
c |     42326 |    8776    20882 |    3539    1920    18927     9.9 |  2.934 % |
c |     42551 |    8776    20882 |    3893    2145    24059    11.2 |  2.934 % |
c ==============================================================================
c [1mFound solution: 43119[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42673 |    8795    20929 |    2931    2267    26056    11.5 |  2.934 % |
c |     42773 |    8795    20929 |    3224    2367    28083    11.9 |  2.963 % |
c |     42923 |    8795    20929 |    3546    2517    30679    12.2 |  2.963 % |
c ==============================================================================
c [1mFound solution: 43117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43127 |    8813    20973 |    2937    2721    35027    12.9 |  2.963 % |
c |     43228 |    8813    20973 |    3230    2822    37238    13.2 |  2.992 % |
c ==============================================================================
c [1mFound solution: 43116[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     43255 |    8839    21037 |    2946    2849    37720    13.2 |  2.992 % |
c |     43355 |    8839    21037 |    3240    2949    39910    13.5 |  3.018 % |
c |     43505 |    8839    21037 |    3564    3099    42423    13.7 |  3.018 % |
c |     43730 |    8839    21037 |    3921    3324    46332    13.9 |  3.018 % |
c ==============================================================================
c [1mFound solution: 43113[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44058 |    8858    21084 |    2952    3652    55120    15.1 |  3.018 % |
c |     44161 |    8858    21084 |    3247    1929    23406    12.1 |  3.046 % |
c |     44314 |    8858    21084 |    3571    2082    28571    13.7 |  3.046 % |
c |     44539 |    8858    21084 |    3929    2307    32117    13.9 |  3.046 % |
c ==============================================================================
c [1mFound solution: 43111[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44731 |    8878    21134 |    2959    2499    36301    14.5 |  3.046 % |
c ==============================================================================
c [1mFound solution: 43110[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44746 |    8896    21178 |    2965    2514    36532    14.5 |  3.046 % |
c |     44846 |    8896    21178 |    3261    2614    38436    14.7 |  3.103 % |
c ==============================================================================
c [1mFound solution: 43108[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44878 |    8915    21225 |    2971    2646    39415    14.9 |  3.103 % |
c |     44978 |    8915    21225 |    3268    2746    40902    14.9 |  3.131 % |
c ==============================================================================
c [1mFound solution: 43106[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45046 |    8927    21255 |    2975    2814    42129    15.0 |  3.131 % |
c |     45146 |    8927    21255 |    3272    2914    44155    15.2 |  3.161 % |
c ==============================================================================
c [1mFound solution: 43105[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45163 |    8944    21298 |    2981    2931    44376    15.1 |  3.161 % |
c ==============================================================================
c [1mFound solution: 43104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45186 |    8960    21338 |    2986    2954    44792    15.2 |  3.161 % |
c |     45286 |    8960    21338 |    3284    3054    46869    15.3 |  3.218 % |
c ==============================================================================
c [1mFound solution: 43103[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45299 |    8976    21378 |    2992    3067    47064    15.3 |  3.218 % |
c |     45399 |    8976    21378 |    3291    3167    48987    15.5 |  3.247 % |
c |     45553 |    8976    21378 |    3620    3321    51608    15.5 |  3.247 % |
c ==============================================================================
c [1mFound solution: 43102[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45561 |    8992    21418 |    2997    3329    51746    15.5 |  3.247 % |
c ==============================================================================
c [1mFound solution: 43100[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45589 |    9010    21464 |    3003    1693    15879     9.4 |  3.247 % |
c ==============================================================================
c [1mFound solution: 43097[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45686 |    9031    21517 |    3010    1790    17366     9.7 |  3.247 % |
c |     45789 |    9031    21517 |    3311    1893    19215    10.2 |  3.331 % |
c |     45939 |    9031    21517 |    3642    2043    21917    10.7 |  3.331 % |
c |     46164 |    9031    21517 |    4006    2268    25807    11.4 |  3.331 % |
c ==============================================================================
c [1mOptimal solution: 43097[0m
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              : 243
c conflicts             : 46470          (1775 /sec)
c decisions             : 66648          (2546 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 26.174 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.86 0.95 0.90 2/54 11606
Raw data (stat): 11606 (runsolver) R 11605 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482070226 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.88 0.96 0.91 2/54 11606
Raw data (stat): 11606 (minisat+) R 11605 24215 24214 0 -1 0 670 0 0 0 995 2 0 0 25 0 1 0 482070226 4374528 648 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1068 648 603 41 0 1027 0
vsize: 4272
[startup+20.0012 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 11606
Raw data (stat): 11606 (minisat+) R 11605 24215 24214 0 -1 0 684 0 0 0 1995 2 0 0 25 0 1 0 482070226 4374528 662 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1068 662 603 41 0 1027 0
vsize: 4272
[startup+26.244 s]
Raw data (loadavg): 0.91 0.96 0.91 1/53 11606
Raw data (stat): 11606 (minisat+) R 11605 24215 24214 0 -1 0 684 0 0 0 1995 2 0 0 25 0 1 0 482070226 4374528 662 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1068 662 603 41 0 1027 0
vsize: 0

Child status: 30
Real time (s): 26.2434
CPU time (s): 26.212
CPU user time (s): 26.177
CPU system time (s): 0.034994
CPU usage (%): 99.8804
Max. virtual memory (Kb): 4272
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	43097
#### END VERIFIER DATA ####