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/MIPLIB/miplib3/normalized-mps-v2-13-7-flugpl.opb
MD5SUM	1b5898327a7b85a882e36ea549878fdf
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1843200
Optimality of the best value was proved	NO
Number of terms in the objective function	195
Biggest coefficient in the objective function	47185920
Number of bits for the biggest coefficient in the objective function	26
Sum of the numbers in the objective function	103639200
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	78643200
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	159755625
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.181972
Number of variables	195
Total number of constraints	29
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	29
Minimum length of a constraint	5
Maximum length of a constraint	45
Trace number 15104

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 03:11:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18367 boxname=wulflinc5 idbench=1413 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1b5898327a7b85a882e36ea549878fdf  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-flugpl.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-flugpl.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-flugpl.opb
IDLAUNCH: 18367
/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:        366816 kB
Buffers:         39564 kB
Cached:         602804 kB
SwapCached:       2272 kB
Active:         235736 kB
Inactive:       411764 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        366564 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14712 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:13:54 (client local time) WITH STATUS 30 IN 117.004 SECONDS
stats: 18367 0 117.004 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 35 PB-constraints to clauses...
c   -- Unit propagations: pp
c   -- Detecting intervals from adjacent constraints: #####
c   -- Clauses(.)/Splits(s): (none)
c ---[  34]---> BDD-cost:    4
c ---[  33]---> BDD-cost:    4
c ---[  32]---> BDD-cost:    4
c ---[  31]---> BDD-cost:    4
c ---[  30]---> BDD-cost:    4
c ---[  29]---> BDD-cost:    4
c ---[  28]---> BDD-cost:    4
c ---[  27]---> BDD-cost:    4
c ---[  26]---> BDD-cost:    4
c ---[  25]---> BDD-cost:    4
c ---[  24]---> BDD-cost:    4
c ---[  20]---> BDD-cost:   20
c ---[  18]---> BDD-cost:   63
c ---[  16]---> BDD-cost:   63
c ---[  14]---> BDD-cost:   63
c ---[  12]---> BDD-cost:   63
c ---[  11]---> BDD-cost:  107
c ---[  10]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[   9]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[   8]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[   7]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[   6]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   86
c ---[   3]---> BDD-cost:   86
c ---[   2]---> BDD-cost:   86
c ---[   1]---> BDD-cost:   86
c ---[   0]---> BDD-cost:   86
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    8270    19747 |    2480       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3210          
c   -- var.elim.:  2000/3210          
c   -- var.elim.:  3000/3210          
c   -- var.elim.:  3210/3210          
c   -- var.elim.:  1000/1572          
c   -- var.elim.:  1572/1572          
c   -- var.elim.:  108/108          
c   -- subsuming                       
c   -- var.elim.:  860/860          
c   -- var.elim.:  329/329          
c   -- subsuming                       
c   -- var.elim.:  99/99          
c   -- var.elim.:  38/38          
c |         0 |    6471    19998 |      --       0       --      -- |     --   | -1799/291
c |         0 |    6471    19998 |    2588       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.52392 s)
c ==============================================================================
c [1mFound solution: 2642432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 9040     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        57 |   29475    73695 |    8842      57      386     6.8 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8379          
c   -- var.elim.:  2000/8379          
c   -- var.elim.:  3000/8379          
c   -- var.elim.:  4000/8379          
c   -- var.elim.:  5000/8379          
c   -- var.elim.:  6000/8379          
c   -- var.elim.:  7000/8379          
c   -- var.elim.:  8000/8379          
c   -- var.elim.:  8379/8379          
c   -- var.elim.:  1000/4655          
c   -- var.elim.:  2000/4655          
c   -- var.elim.:  3000/4655          
c   -- var.elim.:  4000/4655          
c   -- var.elim.:  4655/4655          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  702/702          
c   -- var.elim.:  361/361          
c   -- subsuming                       
c   -- var.elim.:  192/192          
c   -- var.elim.:  10/10          
c |        57 |   26876    83783 |      --      57       --      -- |     --   | -2599/10089
c |        57 |   26876    83783 |   10750      57      386     6.8 |  0.000 % |
c ==============================================================================
c (current CPU-time: 2.18267 s)
c ==============================================================================
c [1mFound solution: 2214118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 5914     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        89 |   41684   115894 |   12505      85      542     6.4 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6869          
c   -- var.elim.:  2000/6869          
c   -- var.elim.:  3000/6869          
c   -- var.elim.:  4000/6869          
c   -- var.elim.:  5000/6869          
c   -- var.elim.:  6000/6869          
c   -- var.elim.:  6869/6869          
c   -- var.elim.:  1000/4129          
c   -- var.elim.:  2000/4129          
c   -- var.elim.:  3000/4129          
c   -- var.elim.:  4000/4129          
c   -- var.elim.:  4129/4129          
c   -- var.elim.:  318/318          
c   -- var.elim.:  155/155          
c   -- var.elim.:  9/9          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  640/640          
c   -- var.elim.:  54/54          
c |        89 |   39556   122276 |      --      85       --      -- |     --   | -2128/6383
c |        89 |   39556   122276 |   15822      71      427     6.0 |  0.000 % |
c ==============================================================================
c (current CPU-time: 3.58745 s)
c ==============================================================================
c [1mFound solution: 2213625[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       155 |   39665   122752 |   11899     136     1100     8.1 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  393/393          
c   -- var.elim.:  298/298          
c |       155 |   39597   123463 |      --     136       --      -- |     --   | -68/712
c |       155 |   39597   123463 |   15838     136     1100     8.1 |  0.000 % |
c |       255 |   39462   122603 |   17363     235     1768     7.5 |  2.188 % |
c ==============================================================================
c (current CPU-time: 4.10637 s)
c ==============================================================================
c [1mFound solution: 2049401[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       394 |   39503   122682 |   11850     367     3417     9.3 |  2.188 % |
c   -- subsuming                       
c   -- var.elim.:  675/675          
c   -- var.elim.:  423/423          
c   -- subsuming                       
c   -- var.elim.:  17/17          
c |       394 |   39387   123409 |      --     367       --      -- |     --   | -115/730
c |       394 |   39387   123409 |   15754     337     2461     7.3 |  2.188 % |
c ==============================================================================
c (current CPU-time: 4.5783 s)
c ==============================================================================
c [1mFound solution: 2049399[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 5947     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       458 |   53612   155652 |   16083     398     5038    12.7 |  2.188 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6821          
c   -- var.elim.:  2000/6821          
c   -- var.elim.:  3000/6821          
c   -- var.elim.:  4000/6821          
c   -- var.elim.:  5000/6821          
c   -- var.elim.:  6000/6821          
c   -- var.elim.:  6821/6821          
c   -- var.elim.:  1000/3572          
c   -- var.elim.:  2000/3572          
c   -- var.elim.:  3000/3572          
c   -- var.elim.:  3572/3572          
c   -- var.elim.:  19/19          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  495/495          
c   -- var.elim.:  93/93          
c |       458 |   51684   161911 |      --     398       --      -- |     --   | -1928/6260
c |       458 |   51684   161911 |   20673     358     4633    12.9 |  2.188 % |
c |       558 |   50367   156613 |   22161     446     5804    13.0 |  4.405 % |
c ==============================================================================
c (current CPU-time: 6.08007 s)
c ==============================================================================
c [1mFound solution: 1979697[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 5600     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       601 |   64361   187040 |   19308     483     6758    14.0 |  4.405 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7903          
c   -- var.elim.:  2000/7903          
c   -- var.elim.:  3000/7903          
c   -- var.elim.:  4000/7903          
c   -- var.elim.:  5000/7903          
c   -- var.elim.:  6000/7903          
c   -- var.elim.:  7000/7903          
c   -- var.elim.:  7903/7903          
c   -- var.elim.:  1000/4728          
c   -- var.elim.:  2000/4728          
c   -- var.elim.:  3000/4728          
c   -- var.elim.:  4000/4728          
c   -- var.elim.:  4728/4728          
c   -- var.elim.:  33/33          
c   -- var.elim.:  18/18          
c   -- var.elim.:  6/6          
c   -- subsuming                       
c   -- var.elim.:  633/633          
c   -- var.elim.:  107/107          
c |       601 |   62343   195657 |      --     483       --      -- |     --   | -2018/8618
c |       601 |   62343   195657 |   24937     398     3854     9.7 |  4.405 % |
c ==============================================================================
c (current CPU-time: 7.99378 s)
c ==============================================================================
c [1mFound solution: 1914159[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 4925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       660 |   65806   190850 |   19741     405     5299    13.1 |  4.405 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10099          
c   -- var.elim.:  2000/10099          
c   -- var.elim.:  3000/10099          
c   -- var.elim.:  4000/10099          
c   -- var.elim.:  5000/10099          
c   -- var.elim.:  6000/10099          
c   -- var.elim.:  7000/10099          
c   -- var.elim.:  8000/10099          
c   -- var.elim.:  9000/10099          
c   -- var.elim.:  10000/10099          
c   -- var.elim.:  10099/10099          
c   -- var.elim.:  1000/5824          
c   -- var.elim.:  2000/5824          
c   -- var.elim.:  3000/5824          
c   -- var.elim.:  4000/5824          
c   -- var.elim.:  5000/5824          
c   -- var.elim.:  5824/5824          
c   -- var.elim.:  641/641          
c   -- var.elim.:  417/417          
c   -- var.elim.:  14/14          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  1000/2502          
c   -- var.elim.:  2000/2502          
c   -- var.elim.:  2502/2502          
c   -- var.elim.:  1000/1801          
c   -- var.elim.:  1801/1801          
c   -- subsuming                       
c   -- var.elim.:  607/607          
c   -- var.elim.:  62/62          
c |       660 |   62015   193274 |      --     405       --      -- |     --   | -3791/2425
c |       660 |   62015   193274 |   24806     326     2489     7.6 |  4.405 % |
c |       762 |   61487   191448 |   27054     423     5681    13.4 | 13.901 % |
c ==============================================================================
c (current CPU-time: 10.8454 s)
c ==============================================================================
c [1mFound solution: 1906842[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3684     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       820 |   70857   213406 |   21257     473     6897    14.6 | 13.901 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4530          
c   -- var.elim.:  2000/4530          
c   -- var.elim.:  3000/4530          
c   -- var.elim.:  4000/4530          
c   -- var.elim.:  4530/4530          
c   -- var.elim.:  1000/2297          
c   -- var.elim.:  2000/2297          
c   -- var.elim.:  2297/2297          
c   -- var.elim.:  107/107          
c   -- var.elim.:  59/59          
c   -- subsuming                       
c   -- var.elim.:  386/386          
c   -- var.elim.:  86/86          
c |       820 |   69505   217284 |      --     473       --      -- |     --   | -1352/3879
c |       820 |   69505   217284 |   27802     468     6823    14.6 | 13.901 % |
c ==============================================================================
c (current CPU-time: 12.1592 s)
c ==============================================================================
c [1mFound solution: 1861850[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3954     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       836 |   76473   227404 |   22941     483     6887    14.3 | 13.901 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6977          
c   -- var.elim.:  2000/6977          
c   -- var.elim.:  3000/6977          
c   -- var.elim.:  4000/6977          
c   -- var.elim.:  5000/6977          
c   -- var.elim.:  6000/6977          
c   -- var.elim.:  6977/6977          
c   -- var.elim.:  1000/4647          
c   -- var.elim.:  2000/4647          
c   -- var.elim.:  3000/4647          
c   -- var.elim.:  4000/4647          
c   -- var.elim.:  4647/4647          
c   -- var.elim.:  610/610          
c   -- var.elim.:  323/323          
c   -- subsuming                       
c   -- var.elim.:  1000/1155          
c   -- var.elim.:  1155/1155          
c   -- var.elim.:  256/256          
c   -- subsuming                       
c   -- var.elim.:  176/176          
c   -- var.elim.:  11/11          
c |       836 |   74689   233617 |      --     483       --      -- |     --   | -1784/6214
c |       836 |   74689   233617 |   29875     414     3294     8.0 | 13.901 % |
c ==============================================================================
c (current CPU-time: 14.3748 s)
c ==============================================================================
c [1mFound solution: 1861786[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       927 |   74761   233896 |   22428     502     6085    12.1 | 13.901 % |
c   -- subsuming                       
c   -- var.elim.:  327/327          
c   -- var.elim.:  223/223          
c |       927 |   74710   234276 |      --     502       --      -- |     --   | -51/381
c |       927 |   74710   234276 |   29884     501     6077    12.1 | 13.901 % |
c |      1027 |   74056   230300 |   32584     589     9823    16.7 | 14.044 % |
c ==============================================================================
c (current CPU-time: 15.5136 s)
c ==============================================================================
c [1mFound solution: 1861785[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3001     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1153 |   81348   247156 |   24404     710    13831    19.5 | 14.044 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4238          
c   -- var.elim.:  2000/4238          
c   -- var.elim.:  3000/4238          
c   -- var.elim.:  4000/4238          
c   -- var.elim.:  4238/4238          
c   -- var.elim.:  1000/3164          
c   -- var.elim.:  2000/3164          
c   -- var.elim.:  3000/3164          
c   -- var.elim.:  3164/3164          
c   -- var.elim.:  272/272          
c   -- var.elim.:  110/110          
c   -- subsuming                       
c   -- var.elim.:  1000/1075          
c   -- var.elim.:  1075/1075          
c   -- var.elim.:  517/517          
c   -- var.elim.:  32/32          
c   -- var.elim.:  28/28          
c   -- subsuming                       
c   -- var.elim.:  475/475          
c   -- var.elim.:  29/29          
c   -- var.elim.:  23/23          
c   -- var.elim.:  44/44          
c   -- var.elim.:  15/15          
c   -- var.elim.:  8/8          
c |      1153 |   80033   250947 |      --     710       --      -- |     --   | -1315/3792
c |      1153 |   80033   250947 |   32013     656     8286    12.6 | 14.044 % |
c |      1253 |   46838   138504 |   20608     684    10375    15.2 | 39.929 % |
c ==============================================================================
c (current CPU-time: 18.1072 s)
c ==============================================================================
c [1mFound solution: 1859805[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2210     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1291 |   52200   150984 |   15659     721    11797    16.4 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11055          
c   -- var.elim.:  2000/11055          
c   -- var.elim.:  3000/11055          
c   -- var.elim.:  4000/11055          
c   -- var.elim.:  5000/11055          
c   -- var.elim.:  6000/11055          
c   -- var.elim.:  7000/11055          
c   -- var.elim.:  8000/11055          
c   -- var.elim.:  9000/11055          
c   -- var.elim.:  10000/11055          
c   -- var.elim.:  11000/11055          
c   -- var.elim.:  11055/11055          
c   -- var.elim.:  1000/7177          
c   -- var.elim.:  2000/7177          
c   -- var.elim.:  3000/7177          
c   -- var.elim.:  4000/7177          
c   -- var.elim.:  5000/7177          
c   -- var.elim.:  6000/7177          
c   -- var.elim.:  7000/7177          
c   -- var.elim.:  7177/7177          
c   -- var.elim.:  1000/1566          
c   -- var.elim.:  1566/1566          
c   -- var.elim.:  1000/1003          
c   -- var.elim.:  1003/1003          
c   -- var.elim.:  420/420          
c   -- var.elim.:  205/205          
c   -- subsuming                       
c   -- var.elim.:  1000/1444          
c   -- var.elim.:  1444/1444          
c   -- var.elim.:  715/715          
c   -- var.elim.:  58/58          
c   -- var.elim.:  63/63          
c   -- subsuming                       
c   -- var.elim.:  455/455          
c   -- var.elim.:  94/94          
c |      1291 |   46835   146144 |      --     721       --      -- |     --   | -5365/-4839
c |      1291 |   46835   146144 |   18734     442     3285     7.4 | 39.929 % |
c ==============================================================================
c (current CPU-time: 20.9858 s)
c ==============================================================================
c [1mFound solution: 1859573[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1321 |   47038   146784 |   14111     472     3918     8.3 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  492/492          
c   -- var.elim.:  328/328          
c   -- var.elim.:  70/70          
c   -- var.elim.:  37/37          
c   -- subsuming                       
c   -- var.elim.:  209/209          
c   -- var.elim.:  22/22          
c   -- var.elim.:  10/10          
c |      1321 |   46805   146339 |      --     472       --      -- |     --   | -232/-442
c |      1321 |   46805   146339 |   18722     470     3895     8.3 | 39.929 % |
c ==============================================================================
c (current CPU-time: 21.8827 s)
c ==============================================================================
c [1mFound solution: 1847525[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1346 |   46968   146866 |   14090     495     4655     9.4 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  357/357          
c   -- var.elim.:  228/228          
c   -- var.elim.:  40/40          
c |      1346 |   46839   146812 |      --     495       --      -- |     --   | -129/-53
c |      1346 |   46839   146812 |   18735     495     4655     9.4 | 39.929 % |
c ==============================================================================
c (current CPU-time: 22.7305 s)
c ==============================================================================
c [1mFound solution: 1847523[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1391 |   46992   147293 |   14097     538     6243    11.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  428/428          
c   -- var.elim.:  227/227          
c   -- var.elim.:  40/40          
c |      1391 |   46864   147214 |      --     538       --      -- |     --   | -128/-78
c |      1391 |   46864   147214 |   18745     531     6198    11.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 23.7494 s)
c ==============================================================================
c [1mFound solution: 1845221[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1473 |   46877   147009 |   14063     610     8542    14.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  465/465          
c   -- var.elim.:  278/278          
c   -- var.elim.:  12/12          
c   -- var.elim.:  114/114          
c   -- subsuming                       
c   -- var.elim.:  157/157          
c   -- var.elim.:  6/6          
c |      1473 |   46742   147049 |      --     610       --      -- |     --   | -135/41
c |      1473 |   46742   147049 |   18696     580     6940    12.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 24.6692 s)
c ==============================================================================
c [1mFound solution: 1845219[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1512 |   46419   145920 |   13925     617     7750    12.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1169          
c   -- var.elim.:  1169/1169          
c   -- var.elim.:  1000/1214          
c   -- var.elim.:  1214/1214          
c   -- var.elim.:  263/263          
c   -- var.elim.:  113/113          
c   -- subsuming                       
c   -- var.elim.:  274/274          
c   -- var.elim.:  7/7          
c |      1512 |   45812   144544 |      --     617       --      -- |     --   | -607/-1375
c |      1512 |   45812   144544 |   18324     607     7589    12.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 25.8011 s)
c ==============================================================================
c [1mFound solution: 1845213[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1582 |   45965   145048 |   13789     677     9982    14.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  340/340          
c   -- var.elim.:  221/221          
c   -- var.elim.:  12/12          
c   -- var.elim.:  113/113          
c |      1582 |   45844   145128 |      --     677       --      -- |     --   | -121/81
c |      1582 |   45844   145128 |   18337     677     9982    14.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 26.6829 s)
c ==============================================================================
c [1mFound solution: 1845211[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1651 |   45991   145609 |   13797     746    12704    17.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  325/325          
c   -- var.elim.:  208/208          
c   -- var.elim.:  12/12          
c   -- var.elim.:  112/112          
c |      1651 |   45871   145581 |      --     746       --      -- |     --   | -120/-27
c |      1651 |   45871   145581 |   18348     746    12704    17.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 27.6298 s)
c ==============================================================================
c [1mFound solution: 1845209[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1739 |   46026   146099 |   13807     834    20177    24.2 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  353/353          
c   -- var.elim.:  231/231          
c   -- var.elim.:  12/12          
c   -- var.elim.:  107/107          
c |      1739 |   45900   146045 |      --     834       --      -- |     --   | -126/-53
c |      1739 |   45900   146045 |   18360     834    20177    24.2 | 39.929 % |
c ==============================================================================
c (current CPU-time: 28.4077 s)
c ==============================================================================
c [1mFound solution: 1845207[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1745 |   46053   146554 |   13815     840    20623    24.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  347/347          
c   -- var.elim.:  226/226          
c   -- var.elim.:  12/12          
c   -- var.elim.:  107/107          
c |      1745 |   45929   146509 |      --     840       --      -- |     --   | -124/-44
c |      1745 |   45929   146509 |   18371     840    20623    24.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 29.1906 s)
c ==============================================================================
c [1mFound solution: 1845107[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1746 |   46081   147011 |   13824     841    20635    24.5 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  341/341          
c   -- var.elim.:  221/221          
c   -- var.elim.:  12/12          
c   -- var.elim.:  95/95          
c |      1746 |   45958   146932 |      --     841       --      -- |     --   | -123/-78
c |      1746 |   45958   146932 |   18383     841    20635    24.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 29.9554 s)
c ==============================================================================
c [1mFound solution: 1845071[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1748 |   46112   147432 |   13833     843    20645    24.5 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  337/337          
c   -- var.elim.:  216/216          
c   -- var.elim.:  12/12          
c   -- var.elim.:  95/95          
c |      1748 |   45988   147369 |      --     843       --      -- |     --   | -124/-62
c |      1748 |   45988   147369 |   18395     843    20645    24.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 30.7143 s)
c ==============================================================================
c [1mFound solution: 1845067[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1748 |   46141   147866 |   13842     843    20645    24.5 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  335/335          
c   -- var.elim.:  215/215          
c   -- var.elim.:  12/12          
c   -- var.elim.:  95/95          
c |      1748 |   46018   147805 |      --     843       --      -- |     --   | -123/-60
c |      1748 |   46018   147805 |   18407     843    20645    24.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 31.4832 s)
c ==============================================================================
c [1mFound solution: 1845035[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1754 |   46170   148300 |   13850     849    20691    24.4 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  334/334          
c   -- var.elim.:  215/215          
c   -- var.elim.:  12/12          
c   -- var.elim.:  95/95          
c |      1754 |   46048   148235 |      --     849       --      -- |     --   | -122/-64
c |      1754 |   46048   148235 |   18419     849    20691    24.4 | 39.929 % |
c ==============================================================================
c (current CPU-time: 32.2531 s)
c ==============================================================================
c [1mFound solution: 1844967[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1756 |   46204   148749 |   13861     851    20700    24.3 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  349/349          
c   -- var.elim.:  226/226          
c   -- var.elim.:  12/12          
c   -- var.elim.:  88/88          
c |      1756 |   46078   148673 |      --     851       --      -- |     --   | -126/-75
c |      1756 |   46078   148673 |   18431     851    20700    24.3 | 39.929 % |
c ==============================================================================
c (current CPU-time: 33.039 s)
c ==============================================================================
c [1mFound solution: 1844699[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1758 |   46228   149159 |   13868     853    20859    24.5 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  327/327          
c   -- var.elim.:  208/208          
c   -- var.elim.:  12/12          
c   -- var.elim.:  112/112          
c |      1758 |   46107   149190 |      --     853       --      -- |     --   | -121/32
c |      1758 |   46107   149190 |   18442     853    20859    24.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 33.8419 s)
c ==============================================================================
c [1mFound solution: 1844697[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1767 |   46256   149669 |   13876     862    21345    24.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  320/320          
c   -- var.elim.:  203/203          
c   -- var.elim.:  12/12          
c   -- var.elim.:  107/107          
c |      1767 |   46136   149698 |      --     862       --      -- |     --   | -120/30
c |      1767 |   46136   149698 |   18454     862    21345    24.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 34.6267 s)
c ==============================================================================
c [1mFound solution: 1844599[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1767 |   46294   150216 |   13888     862    21345    24.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  350/350          
c   -- var.elim.:  225/225          
c   -- var.elim.:  12/12          
c   -- var.elim.:  129/129          
c |      1767 |   46167   150353 |      --     862       --      -- |     --   | -127/138
c |      1767 |   46167   150353 |   18466     862    21345    24.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 35.4266 s)
c ==============================================================================
c [1mFound solution: 1844597[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1767 |   46323   150863 |   13896     862    21345    24.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  344/344          
c   -- var.elim.:  221/221          
c   -- var.elim.:  12/12          
c   -- var.elim.:  125/125          
c |      1767 |   46198   151000 |      --     862       --      -- |     --   | -125/138
c |      1767 |   46198   151000 |   18479     862    21345    24.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 36.2285 s)
c ==============================================================================
c [1mFound solution: 1844595[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1767 |   46345   151463 |   13903     862    21345    24.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  306/306          
c   -- var.elim.:  191/191          
c   -- var.elim.:  12/12          
c   -- var.elim.:  95/95          
c |      1767 |   46227   151484 |      --     862       --      -- |     --   | -118/22
c |      1767 |   46227   151484 |   18490     862    21345    24.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 37.0224 s)
c ==============================================================================
c [1mFound solution: 1844473[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1767 |   46385   152007 |   13915     862    21345    24.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  355/355          
c   -- var.elim.:  231/231          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1767 |   46256   151807 |      --     862       --      -- |     --   | -129/-199
c |      1767 |   46256   151807 |   18502     862    21345    24.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 37.8342 s)
c ==============================================================================
c [1mFound solution: 1844471[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1767 |   46413   152323 |   13923     862    21345    24.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  349/349          
c   -- var.elim.:  226/226          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1767 |   46286   152179 |      --     862       --      -- |     --   | -127/-143
c |      1767 |   46286   152179 |   18514     862    21345    24.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 38.6361 s)
c ==============================================================================
c [1mFound solution: 1844469[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1767 |   46441   152687 |   13932     862    21345    24.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  343/343          
c   -- var.elim.:  222/222          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1767 |   46316   152547 |      --     862       --      -- |     --   | -125/-139
c |      1767 |   46316   152547 |   18526     862    21345    24.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 39.438 s)
c ==============================================================================
c [1mFound solution: 1844467[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1767 |   46470   153052 |   13940     862    21345    24.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  341/341          
c   -- var.elim.:  221/221          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1767 |   46346   152914 |      --     862       --      -- |     --   | -124/-137
c |      1767 |   46346   152914 |   18538     862    21345    24.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 40.2559 s)
c ==============================================================================
c [1mFound solution: 1844441[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1779 |   46496   153394 |   13948     874    22269    25.5 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  320/320          
c   -- var.elim.:  204/204          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1779 |   46376   153264 |      --     874       --      -- |     --   | -120/-129
c |      1779 |   46376   153264 |   18550     874    22269    25.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 41.0628 s)
c ==============================================================================
c [1mFound solution: 1844439[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1783 |   46526   153744 |   13957     878    22655    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  320/320          
c   -- var.elim.:  204/204          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1783 |   46406   153614 |      --     878       --      -- |     --   | -120/-129
c |      1783 |   46406   153614 |   18562     878    22655    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 41.8716 s)
c ==============================================================================
c [1mFound solution: 1844437[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1784 |   46563   154125 |   13968     879    22699    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  344/344          
c   -- var.elim.:  222/222          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1784 |   46437   153995 |      --     879       --      -- |     --   | -126/-129
c |      1784 |   46437   153995 |   18574     879    22699    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 42.6955 s)
c ==============================================================================
c [1mFound solution: 1844435[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1784 |   46593   154503 |   13977     879    22699    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  342/342          
c   -- var.elim.:  221/221          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1784 |   46468   154375 |      --     879       --      -- |     --   | -125/-127
c |      1784 |   46468   154375 |   18587     879    22699    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 43.5164 s)
c ==============================================================================
c [1mFound solution: 1844433[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1784 |   46623   154876 |   13986     879    22699    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  336/336          
c   -- var.elim.:  216/216          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1784 |   46499   154750 |      --     879       --      -- |     --   | -124/-125
c |      1784 |   46499   154750 |   18599     879    22699    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 44.3373 s)
c ==============================================================================
c [1mFound solution: 1844431[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1784 |   46655   155253 |   13996     879    22699    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  337/337          
c   -- var.elim.:  216/216          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1784 |   46530   155125 |      --     879       --      -- |     --   | -125/-127
c |      1784 |   46530   155125 |   18612     879    22699    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 45.1551 s)
c ==============================================================================
c [1mFound solution: 1844429[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1784 |   46688   155637 |   14006     879    22699    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  344/344          
c   -- var.elim.:  222/222          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1784 |   46562   155525 |      --     879       --      -- |     --   | -126/-111
c |      1784 |   46562   155525 |   18624     879    22699    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 45.978 s)
c ==============================================================================
c [1mFound solution: 1844427[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1784 |   46717   156025 |   14015     879    22699    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  335/335          
c   -- var.elim.:  215/215          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1784 |   46593   155899 |      --     879       --      -- |     --   | -124/-125
c |      1784 |   46593   155899 |   18637     879    22699    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 46.8009 s)
c ==============================================================================
c [1mFound solution: 1844425[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1786 |   46753   156424 |   14025     881    22721    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  355/355          
c   -- var.elim.:  231/231          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1786 |   46625   156302 |      --     881       --      -- |     --   | -128/-121
c |      1786 |   46625   156302 |   18650     881    22721    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 47.6288 s)
c ==============================================================================
c [1mFound solution: 1844419[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1787 |   46778   156793 |   14033     882    22729    25.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  328/328          
c   -- var.elim.:  210/210          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1787 |   46656   156671 |      --     882       --      -- |     --   | -122/-121
c |      1787 |   46656   156671 |   18662     882    22729    25.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 48.4606 s)
c ==============================================================================
c [1mFound solution: 1844417[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1790 |   46811   157171 |   14043     885    22768    25.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  335/335          
c   -- var.elim.:  216/216          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1790 |   46688   157059 |      --     885       --      -- |     --   | -123/-111
c |      1790 |   46688   157059 |   18675     885    22768    25.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 49.2705 s)
c ==============================================================================
c [1mFound solution: 1844415[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1793 |   46843   157559 |   14052     888    22803    25.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  335/335          
c   -- var.elim.:  216/216          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1793 |   46720   157447 |      --     888       --      -- |     --   | -123/-111
c |      1793 |   46720   157447 |   18688     888    22803    25.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 50.1104 s)
c ==============================================================================
c [1mFound solution: 1844413[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1800 |   46873   157938 |   14061     895    23881    26.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  328/328          
c   -- var.elim.:  210/210          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1800 |   46751   157816 |      --     895       --      -- |     --   | -122/-121
c |      1800 |   46751   157816 |   18700     895    23881    26.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 50.9353 s)
c ==============================================================================
c [1mFound solution: 1844411[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1803 |   46901   158295 |   14070     898    23902    26.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  319/319          
c   -- var.elim.:  203/203          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1803 |   46781   158165 |      --     898       --      -- |     --   | -120/-129
c |      1803 |   46781   158165 |   18712     898    23902    26.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 51.7731 s)
c ==============================================================================
c [1mFound solution: 1844329[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1809 |   46941   158690 |   14082     904    24400    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  355/355          
c   -- var.elim.:  231/231          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1809 |   46813   158556 |      --     904       --      -- |     --   | -128/-133
c |      1809 |   46813   158556 |   18725     904    24400    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 52.622 s)
c ==============================================================================
c [1mFound solution: 1844327[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1821 |   46971   159072 |   14091     916    24809    27.1 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  348/348          
c   -- var.elim.:  226/226          
c   -- var.elim.:  12/12          
c   -- var.elim.:  75/75          
c |      1821 |   46845   158942 |      --     916       --      -- |     --   | -126/-129
c |      1821 |   46845   158942 |   18738     916    24809    27.1 | 39.929 % |
c ==============================================================================
c (current CPU-time: 53.4969 s)
c ==============================================================================
c [1mFound solution: 1844325[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1842 |   46855   157164 |   14056     936    25655    27.4 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  409/409          
c   -- var.elim.:  254/254          
c   -- var.elim.:  12/12          
c   -- var.elim.:  72/72          
c |      1842 |   46732   157321 |      --     936       --      -- |     --   | -123/158
c |      1842 |   46732   157321 |   18692     879    20075    22.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 54.3687 s)
c ==============================================================================
c [1mFound solution: 1844091[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1855 |   46876   157782 |   14062     892    21438    24.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  314/314          
c   -- var.elim.:  193/193          
c   -- var.elim.:  12/12          
c   -- var.elim.:  97/97          
c |      1855 |   46756   157677 |      --     892       --      -- |     --   | -120/-104
c |      1855 |   46756   157677 |   18702     892    21438    24.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 55.2176 s)
c ==============================================================================
c [1mFound solution: 1843963[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1864 |   46899   158130 |   14069     901    22034    24.5 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  300/300          
c   -- var.elim.:  187/187          
c   -- var.elim.:  12/12          
c   -- var.elim.:  91/91          
c |      1864 |   46782   158032 |      --     901       --      -- |     --   | -117/-97
c |      1864 |   46782   158032 |   18712     901    22034    24.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 56.1695 s)
c ==============================================================================
c [1mFound solution: 1843947[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1898 |   46933   158524 |   14079     935    25354    27.1 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  331/331          
c   -- var.elim.:  211/211          
c   -- var.elim.:  12/12          
c   -- var.elim.:  115/115          
c |      1898 |   46810   158523 |      --     935       --      -- |     --   | -123/0
c |      1898 |   46810   158523 |   18724     935    25354    27.1 | 39.929 % |
c ==============================================================================
c (current CPU-time: 57.0323 s)
c ==============================================================================
c [1mFound solution: 1843819[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1899 |   46962   159016 |   14088     936    25573    27.3 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  331/331          
c   -- var.elim.:  212/212          
c   -- var.elim.:  12/12          
c   -- var.elim.:  85/85          
c |      1899 |   46839   158900 |      --     936       --      -- |     --   | -123/-115
c |      1899 |   46839   158900 |   18735     936    25573    27.3 | 39.929 % |
c ==============================================================================
c (current CPU-time: 57.8892 s)
c ==============================================================================
c [1mFound solution: 1843803[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1899 |   46989   159383 |   14096     936    25573    27.3 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  323/323          
c   -- var.elim.:  206/206          
c   -- var.elim.:  12/12          
c   -- var.elim.:  85/85          
c |      1899 |   46868   159271 |      --     936       --      -- |     --   | -121/-111
c |      1899 |   46868   159271 |   18747     936    25573    27.3 | 39.929 % |
c ==============================================================================
c (current CPU-time: 58.7291 s)
c ==============================================================================
c [1mFound solution: 1843771[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1901 |   47016   159744 |   14104     938    25608    27.3 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  315/315          
c   -- var.elim.:  200/200          
c   -- var.elim.:  12/12          
c   -- var.elim.:  85/85          
c |      1901 |   46897   159636 |      --     938       --      -- |     --   | -119/-107
c |      1901 |   46897   159636 |   18758     938    25608    27.3 | 39.929 % |
c ==============================================================================
c (current CPU-time: 59.5819 s)
c ==============================================================================
c [1mFound solution: 1843723[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1904 |   47050   160129 |   14114     941    25663    27.3 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  330/330          
c   -- var.elim.:  212/212          
c   -- var.elim.:  12/12          
c   -- var.elim.:  85/85          
c |      1904 |   46928   160015 |      --     941       --      -- |     --   | -122/-113
c |      1904 |   46928   160015 |   18771     941    25663    27.3 | 39.929 % |
c ==============================================================================
c (current CPU-time: 60.4478 s)
c ==============================================================================
c [1mFound solution: 1843707[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1907 |   47069   160457 |   14120     944    25670    27.2 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  291/291          
c   -- var.elim.:  180/180          
c   -- var.elim.:  12/12          
c   -- var.elim.:  84/84          
c |      1907 |   46954   160356 |      --     944       --      -- |     --   | -115/-100
c |      1907 |   46954   160356 |   18781     944    25670    27.2 | 39.929 % |
c ==============================================================================
c (current CPU-time: 61.2877 s)
c ==============================================================================
c [1mFound solution: 1843659[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1907 |   47106   160849 |   14131     944    25670    27.2 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  331/331          
c   -- var.elim.:  211/211          
c   -- var.elim.:  12/12          
c   -- var.elim.:  115/115          
c |      1907 |   46982   160815 |      --     944       --      -- |     --   | -124/-33
c |      1907 |   46982   160815 |   18792     944    25670    27.2 | 39.929 % |
c ==============================================================================
c (current CPU-time: 62.1615 s)
c ==============================================================================
c [1mFound solution: 1843627[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1907 |   47133   161306 |   14139     944    25670    27.2 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  330/330          
c   -- var.elim.:  211/211          
c   -- var.elim.:  12/12          
c   -- var.elim.:  115/115          
c |      1907 |   47010   161268 |      --     944       --      -- |     --   | -123/-37
c |      1907 |   47010   161268 |   18804     944    25670    27.2 | 39.929 % |
c ==============================================================================
c (current CPU-time: 63.0434 s)
c ==============================================================================
c [1mFound solution: 1843611[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1907 |   47159   161749 |   14147     944    25670    27.2 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  322/322          
c   -- var.elim.:  205/205          
c   -- var.elim.:  12/12          
c   -- var.elim.:  109/109          
c |      1907 |   47038   161715 |      --     944       --      -- |     --   | -121/-33
c |      1907 |   47038   161715 |   18815     944    25670    27.2 | 39.929 % |
c ==============================================================================
c (current CPU-time: 63.9113 s)
c ==============================================================================
c [1mFound solution: 1843595[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1908 |   47190   162207 |   14156     945    25951    27.5 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  330/330          
c   -- var.elim.:  211/211          
c   -- var.elim.:  12/12          
c   -- var.elim.:  115/115          
c |      1908 |   47067   162215 |      --     945       --      -- |     --   | -123/9
c |      1908 |   47067   162215 |   18826     945    25951    27.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 64.7971 s)
c ==============================================================================
c [1mFound solution: 1843579[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1908 |   47212   162677 |   14163     945    25951    27.5 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  307/307          
c   -- var.elim.:  193/193          
c   -- var.elim.:  12/12          
c   -- var.elim.:  97/97          
c |      1908 |   47094   162603 |      --     945       --      -- |     --   | -118/-73
c |      1908 |   47094   162603 |   18837     945    25951    27.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 65.678 s)
c ==============================================================================
c [1mFound solution: 1843577[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1914 |   47251   163122 |   14175     951    25973    27.3 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  352/352          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  131/131          
c |      1914 |   47122   163066 |      --     951       --      -- |     --   | -129/-55
c |      1914 |   47122   163066 |   18848     951    25973    27.3 | 39.929 % |
c ==============================================================================
c (current CPU-time: 66.5859 s)
c ==============================================================================
c [1mFound solution: 1843575[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1921 |   47278   163578 |   14183     958    26677    27.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  346/346          
c   -- var.elim.:  222/222          
c   -- var.elim.:  12/12          
c   -- var.elim.:  126/126          
c |      1921 |   47150   163524 |      --     958       --      -- |     --   | -128/-53
c |      1921 |   47150   163524 |   18860     958    26677    27.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 67.4867 s)
c ==============================================================================
c [1mFound solution: 1843574[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1925 |   47303   164026 |   14190     962    26689    27.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  339/339          
c   -- var.elim.:  218/218          
c   -- var.elim.:  12/12          
c   -- var.elim.:  122/122          
c |      1925 |   47178   163978 |      --     962       --      -- |     --   | -125/-47
c |      1925 |   47178   163978 |   18871     962    26689    27.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 68.3866 s)
c ==============================================================================
c [1mFound solution: 1843573[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1926 |   47333   164484 |   14199     963    26691    27.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  341/341          
c   -- var.elim.:  218/218          
c   -- var.elim.:  12/12          
c   -- var.elim.:  122/122          
c |      1926 |   47206   164432 |      --     963       --      -- |     --   | -127/-51
c |      1926 |   47206   164432 |   18882     963    26691    27.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 69.2815 s)
c ==============================================================================
c [1mFound solution: 1843561[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1927 |   47364   164952 |   14209     964    26767    27.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  352/352          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  131/131          
c |      1927 |   47235   164948 |      --     964       --      -- |     --   | -129/-3
c |      1927 |   47235   164948 |   18894     964    26767    27.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 70.2013 s)
c ==============================================================================
c [1mFound solution: 1843558[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1929 |   47390   165453 |   14216     966    26839    27.8 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  340/340          
c   -- var.elim.:  218/218          
c   -- var.elim.:  12/12          
c   -- var.elim.:  122/122          
c |      1929 |   47264   165455 |      --     966       --      -- |     --   | -126/3
c |      1929 |   47264   165455 |   18905     966    26839    27.8 | 39.929 % |
c ==============================================================================
c (current CPU-time: 71.1202 s)
c ==============================================================================
c [1mFound solution: 1843557[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1931 |   47414   165939 |   14224     968    26855    27.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  324/324          
c   -- var.elim.:  206/206          
c   -- var.elim.:  12/12          
c   -- var.elim.:  110/110          
c |      1931 |   47292   165897 |      --     968       --      -- |     --   | -122/-41
c |      1931 |   47292   165897 |   18916     968    26855    27.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 72.0171 s)
c ==============================================================================
c [1mFound solution: 1843554[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1937 |   47452   166423 |   14235     974    26932    27.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  356/356          
c   -- var.elim.:  230/230          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      1937 |   47322   166469 |      --     974       --      -- |     --   | -130/47
c |      1937 |   47322   166469 |   18928     974    26932    27.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 72.9409 s)
c ==============================================================================
c [1mFound solution: 1843546[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1941 |   47482   166996 |   14244     978    26953    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  357/357          
c   -- var.elim.:  230/230          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      1941 |   47351   166982 |      --     978       --      -- |     --   | -131/-13
c |      1941 |   47351   166982 |   18940     978    26953    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 73.8808 s)
c ==============================================================================
c [1mFound solution: 1843530[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1942 |   47512   167510 |   14253     979    27003    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  357/357          
c   -- var.elim.:  230/230          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      1942 |   47381   167542 |      --     979       --      -- |     --   | -131/33
c |      1942 |   47381   167542 |   18952     979    27003    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 74.8276 s)
c ==============================================================================
c [1mFound solution: 1843522[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1944 |   47543   168071 |   14262     981    27063    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  357/357          
c   -- var.elim.:  230/230          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      1944 |   47412   168149 |      --     981       --      -- |     --   | -131/79
c |      1944 |   47412   168149 |   18964     981    27063    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 75.9675 s)
c ==============================================================================
c [1mFound solution: 1843521[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1993 |   47566   168645 |   14269    1030    29155    28.3 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  332/332          
c   -- var.elim.:  212/212          
c   -- var.elim.:  12/12          
c   -- var.elim.:  116/116          
c |      1993 |   47442   168691 |      --    1030       --      -- |     --   | -124/47
c |      1993 |   47442   168691 |   18976    1030    29155    28.3 | 39.929 % |
c ==============================================================================
c (current CPU-time: 77.0293 s)
c ==============================================================================
c [1mFound solution: 1843518[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2020 |   47514   168529 |   14254    1056    30822    29.2 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  467/467          
c   -- var.elim.:  242/242          
c   -- var.elim.:  12/12          
c   -- var.elim.:  122/122          
c |      2020 |   47385   168650 |      --    1056       --      -- |     --   | -129/122
c |      2020 |   47385   168650 |   18954     996    24407    24.5 | 39.929 % |
c ==============================================================================
c (current CPU-time: 78.2081 s)
c ==============================================================================
c [1mFound solution: 1843517[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2071 |   47533   169117 |   14259    1046    26903    25.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  338/338          
c   -- var.elim.:  203/203          
c   -- var.elim.:  12/12          
c   -- var.elim.:  110/110          
c |      2071 |   47410   169102 |      --    1046       --      -- |     --   | -123/-14
c |      2071 |   47410   169102 |   18964    1046    26903    25.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 79.189 s)
c ==============================================================================
c [1mFound solution: 1843516[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2081 |   47572   169626 |   14271    1056    28154    26.7 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  352/352          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2081 |   47443   169797 |      --    1056       --      -- |     --   | -129/172
c |      2081 |   47443   169797 |   18977    1056    28154    26.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 80.1738 s)
c ==============================================================================
c [1mFound solution: 1843514[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2083 |   47603   170321 |   14280    1058    28521    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  354/354          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2083 |   47472   170298 |      --    1058       --      -- |     --   | -131/-22
c |      2083 |   47472   170298 |   18988    1058    28521    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 81.1687 s)
c ==============================================================================
c [1mFound solution: 1843498[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2083 |   47633   170823 |   14289    1058    28521    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  354/354          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2083 |   47502   170846 |      --    1058       --      -- |     --   | -131/24
c |      2083 |   47502   170846 |   19000    1058    28521    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 82.1565 s)
c ==============================================================================
c [1mFound solution: 1843490[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2083 |   47663   171370 |   14298    1058    28521    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  353/353          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2083 |   47533   171441 |      --    1058       --      -- |     --   | -130/72
c |      2083 |   47533   171441 |   19013    1058    28521    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 83.1514 s)
c ==============================================================================
c [1mFound solution: 1843482[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2083 |   47680   171904 |   14303    1058    28521    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  306/306          
c   -- var.elim.:  191/191          
c   -- var.elim.:  12/12          
c   -- var.elim.:  98/98          
c |      2083 |   47561   171865 |      --    1058       --      -- |     --   | -119/-38
c |      2083 |   47561   171865 |   19024    1058    28521    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 84.1182 s)
c ==============================================================================
c [1mFound solution: 1843474[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2085 |   47722   172389 |   14316    1060    28645    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  353/353          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2085 |   47592   172454 |      --    1060       --      -- |     --   | -130/66
c |      2085 |   47592   172454 |   19036    1060    28645    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 85.1451 s)
c ==============================================================================
c [1mFound solution: 1843466[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2092 |   47754   172980 |   14326    1067    28780    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  354/354          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2092 |   47623   173037 |      --    1067       --      -- |     --   | -131/58
c |      2092 |   47623   173037 |   19049    1067    28780    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 86.1469 s)
c ==============================================================================
c [1mFound solution: 1843458[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2092 |   47786   173564 |   14335    1067    28780    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  354/354          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2092 |   47655   173661 |      --    1067       --      -- |     --   | -131/98
c |      2092 |   47655   173661 |   19062    1067    28780    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 87.1488 s)
c ==============================================================================
c [1mFound solution: 1843457[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2092 |   47809   174153 |   14342    1067    28780    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  328/328          
c   -- var.elim.:  209/209          
c   -- var.elim.:  12/12          
c   -- var.elim.:  116/116          
c |      2092 |   47686   174226 |      --    1067       --      -- |     --   | -123/74
c |      2092 |   47686   174226 |   19074    1067    28780    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 88.1536 s)
c ==============================================================================
c [1mFound solution: 1843456[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2092 |   47830   174678 |   14348    1067    28780    27.0 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  298/298          
c   -- var.elim.:  185/185          
c   -- var.elim.:  12/12          
c   -- var.elim.:  92/92          
c |      2092 |   47713   174603 |      --    1067       --      -- |     --   | -117/-74
c |      2092 |   47713   174603 |   19085    1067    28780    27.0 | 39.929 % |
c ==============================================================================
c (current CPU-time: 89.1594 s)
c ==============================================================================
c [1mFound solution: 1843450[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2110 |   47871   175124 |   14361    1085    29506    27.2 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  353/353          
c   -- var.elim.:  227/227          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2110 |   47741   175056 |      --    1085       --      -- |     --   | -130/-67
c |      2110 |   47741   175056 |   19096    1085    29506    27.2 | 39.929 % |
c ==============================================================================
c (current CPU-time: 90.2653 s)
c ==============================================================================
c [1mFound solution: 1843434[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2143 |   47895   175167 |   14368    1117    30869    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  432/432          
c   -- var.elim.:  235/235          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2143 |   47764   175148 |      --    1117       --      -- |     --   | -131/-18
c |      2143 |   47764   175148 |   19105    1116    30867    27.7 | 39.929 % |
c ==============================================================================
c (current CPU-time: 91.3271 s)
c ==============================================================================
c [1mFound solution: 1843418[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2149 |   47924   175670 |   14377    1122    30998    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  352/352          
c   -- var.elim.:  225/225          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2149 |   47793   175642 |      --    1122       --      -- |     --   | -131/-27
c |      2149 |   47793   175642 |   19117    1122    30998    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 92.368 s)
c ==============================================================================
c [1mFound solution: 1843402[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   47954   176165 |   14386    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  352/352          
c   -- var.elim.:  225/225          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2150 |   47823   176182 |      --    1123       --      -- |     --   | -131/18
c |      2150 |   47823   176182 |   19129    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 93.4128 s)
c ==============================================================================
c [1mFound solution: 1843322[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   47982   176702 |   14394    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  351/351          
c   -- var.elim.:  225/225          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2150 |   47852   176664 |      --    1123       --      -- |     --   | -130/-37
c |      2150 |   47852   176664 |   19140    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 94.4536 s)
c ==============================================================================
c [1mFound solution: 1843305[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   47986   177076 |   14395    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  268/268          
c   -- var.elim.:  163/163          
c   -- var.elim.:  12/12          
c   -- var.elim.:  72/72          
c |      2150 |   47877   176941 |      --    1123       --      -- |     --   | -109/-134
c |      2150 |   47877   176941 |   19150    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 95.4395 s)
c ==============================================================================
c [1mFound solution: 1843289[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48025   177409 |   14407    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  310/310          
c   -- var.elim.:  195/195          
c   -- var.elim.:  12/12          
c   -- var.elim.:  104/104          
c |      2150 |   47906   177393 |      --    1123       --      -- |     --   | -119/-15
c |      2150 |   47906   177393 |   19162    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 96.4533 s)
c ==============================================================================
c [1mFound solution: 1843273[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48065   177908 |   14419    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  346/346          
c   -- var.elim.:  222/222          
c   -- var.elim.:  12/12          
c   -- var.elim.:  131/131          
c |      2150 |   47937   177952 |      --    1123       --      -- |     --   | -128/45
c |      2150 |   47937   177952 |   19174    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 97.5242 s)
c ==============================================================================
c [1mFound solution: 1843265[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48091   178442 |   14427    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  326/326          
c   -- var.elim.:  207/207          
c   -- var.elim.:  12/12          
c   -- var.elim.:  116/116          
c |      2150 |   47968   178496 |      --    1123       --      -- |     --   | -123/55
c |      2150 |   47968   178496 |   19187    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 98.567 s)
c ==============================================================================
c [1mFound solution: 1843257[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48125   179008 |   14437    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  345/345          
c   -- var.elim.:  222/222          
c   -- var.elim.:  12/12          
c   -- var.elim.:  131/131          
c |      2150 |   47998   179009 |      --    1123       --      -- |     --   | -127/2
c |      2150 |   47998   179009 |   19199    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 99.6269 s)
c ==============================================================================
c [1mFound solution: 1843241[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48156   179522 |   14446    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  345/345          
c   -- var.elim.:  222/222          
c   -- var.elim.:  12/12          
c   -- var.elim.:  131/131          
c |      2150 |   48029   179562 |      --    1123       --      -- |     --   | -127/41
c |      2150 |   48029   179562 |   19211    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 100.693 s)
c ==============================================================================
c [1mFound solution: 1843225[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48178   180031 |   14453    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  310/310          
c   -- var.elim.:  195/195          
c   -- var.elim.:  12/12          
c   -- var.elim.:  104/104          
c |      2150 |   48059   180048 |      --    1123       --      -- |     --   | -119/18
c |      2150 |   48059   180048 |   19223    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 101.724 s)
c ==============================================================================
c [1mFound solution: 1843217[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48212   180536 |   14463    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  325/325          
c   -- var.elim.:  207/207          
c   -- var.elim.:  12/12          
c   -- var.elim.:  116/116          
c |      2150 |   48090   180580 |      --    1123       --      -- |     --   | -122/45
c |      2150 |   48090   180580 |   19236    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 102.778 s)
c ==============================================================================
c [1mFound solution: 1843210[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48252   181103 |   14475    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  351/351          
c   -- var.elim.:  225/225          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2150 |   48122   181164 |      --    1123       --      -- |     --   | -130/62
c |      2150 |   48122   181164 |   19248    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 103.849 s)
c ==============================================================================
c [1mFound solution: 1843209[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48281   181678 |   14484    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  345/345          
c   -- var.elim.:  222/222          
c   -- var.elim.:  12/12          
c   -- var.elim.:  131/131          
c |      2150 |   48154   181745 |      --    1123       --      -- |     --   | -127/68
c |      2150 |   48154   181745 |   19261    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 104.95 s)
c ==============================================================================
c [1mFound solution: 1843202[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48317   182269 |   14495    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  351/351          
c   -- var.elim.:  225/225          
c   -- var.elim.:  12/12          
c   -- var.elim.:  134/134          
c |      2150 |   48187   182363 |      --    1123       --      -- |     --   | -130/95
c |      2150 |   48187   182363 |   19274    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 106.047 s)
c ==============================================================================
c [1mFound solution: 1843201[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48341   182852 |   14502    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  325/325          
c   -- var.elim.:  207/207          
c   -- var.elim.:  12/12          
c   -- var.elim.:  116/116          
c |      2150 |   48219   182929 |      --    1123       --      -- |     --   | -122/78
c |      2150 |   48219   182929 |   19287    1123    31018    27.6 | 39.929 % |
c ==============================================================================
c (current CPU-time: 107.132 s)
c ==============================================================================
c [1mFound solution: 1843200[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2150 |   48363   183378 |   14508    1123    31018    27.6 | 39.929 % |
c   -- subsuming                       
c   -- var.elim.:  295/295          
c   -- var.elim.:  183/183          
c   -- var.elim.:  12/12          
c   -- var.elim.:  92/92          
c |      2150 |   48247   183335 |      --    1123       --      -- |     --   | -116/-42
c |      2150 |   48247   183335 |   19298    1123    31018    27.6 | 39.929 % |
c |      2251 |   48106   178129 |   21166    1221    37244    30.5 | 44.830 % |
c ==============================================================================
c [1mOptimal solution: 1843200[0m
s OPTIMUM FOUND
v -STM1_bit_7 -STM1_bit_6 -STM1_bit_5 -STM1_bit_4 -STM1_bit_3 -STM1_bit_2 -STM1_bit_1 -STM1_bit0 -STM1_bit1 STM1_bit2 STM1_bit3 STM1_bit4 STM1_bit5 -STM1_bit6 -STM1_bit7 -STM1_bit8 -STM1_bit9 -STM1_bit10 -STM1_bit11 -STM1_bit12 -ANM1_bit0 ANM1_bit1 ANM1_bit2 -ANM1_bit3 -ANM1_bit4 -UE1_bit_7 -UE1_bit_6 -UE1_bit_5 -UE1_bit_4 -UE1_bit_3 -UE1_bit_2 -UE1_bit_1 -UE1_bit0 -UE1_bit1 -UE1_bit2 -UE1_bit3 -UE1_bit4 -UE1_bit5 -UE1_bit6 -UE1_bit7 -UE1_bit8 -UE1_bit9 -UE1_bit10 -UE1_bit11 -UE1_bit12 STM2_bit0 STM2_bit1 -STM2_bit2 -STM2_bit3 -STM2_bit4 -ANM2_bit0 ANM2_bit1 ANM2_bit2 -ANM2_bit3 -ANM2_bit4 -UE2_bit_7 -UE2_bit_6 -UE2_bit_5 -UE2_bit_4 -UE2_bit_3 -UE2_bit_2 -UE2_bit_1 -UE2_bit0 -UE2_bit1 -UE2_bit2 UE2_bit3 UE2_bit4 -UE2_bit5 UE2_bit6 -UE2_bit7 -UE2_bit8 UE2_bit9 -UE2_bit10 -UE2_bit11 -UE2_bit12 STM3_bit0 STM3_bit1 -STM3_bit2 -STM3_bit3 -STM3_bit4 -ANM3_bit0 -ANM3_bit1 -ANM3_bit2 -ANM3_bit3 ANM3_bit4 -UE3_bit_7 -UE3_bit_6 -UE3_bit_5 -UE3_bit_4 -UE3_bit_3 -UE3_bit_2 -UE3_bit_1 -UE3_bit0 -UE3_bit1 -UE3_bit2 UE3_bit3 UE3_bit4 -UE3_bit5 UE3_bit6 -UE3_bit7 -UE3_bit8 UE3_bit9 -UE3_bit10 -UE3_bit11 -UE3_bit12 STM4_bit0 -STM4_bit1 STM4_bit2 STM4_bit3 -STM4_bit4 ANM4_bit0 ANM4_bit1 ANM4_bit2 -ANM4_bit3 -ANM4_bit4 -UE4_bit_7 -UE4_bit_6 -UE4_bit_5 -UE4_bit_4 -UE4_bit_3 -UE4_bit_2 -UE4_bit_1 -UE4_bit0 -UE4_bit1 -UE4_bit2 UE4_bit3 -UE4_bit4 -UE4_bit5 UE4_bit6 UE4_bit7 -UE4_bit8 -UE4_bit9 -UE4_bit10 -UE4_bit11 -UE4_bit12 STM5_bit0 -STM5_bit1 STM5_bit2 STM5_bit3 -STM5_bit4 -ANM5_bit0 -ANM5_bit1 ANM5_bit2 ANM5_bit3 -ANM5_bit4 -UE5_bit_7 -UE5_bit_6 -UE5_bit_5 -UE5_bit_4 -UE5_bit_3 -UE5_bit_2 -UE5_bit_1 -UE5_bit0 -UE5_bit1 -UE5_bit2 -UE5_bit3 -UE5_bit4 -UE5_bit5 -UE5_bit6 -UE5_bit7 -UE5_bit8 -UE5_bit9 -UE5_bit10 -UE5_bit11 -UE5_bit12 -STM6_bit0 STM6_bit1 -STM6_bit2 -STM6_bit3 STM6_bit4 -ANM6_bit0 -ANM6_bit1 -ANM6_bit2 -ANM6_bit3 -ANM6_bit4 -UE6_bit_7 -UE6_bit_6 -UE6_bit_5 -UE6_bit_4 -UE6_bit_3 -UE6_bit_2 -UE6_bit_1 -UE6_bit0 UE6_bit1 UE6_bit2 UE6_bit3 -UE6_bit4 UE6_bit5 UE6_bit6 UE6_bit7 -UE6_bit8 UE6_bit9 -UE6_bit10 -UE6_bit11 -UE6_bit12
c _______________________________________________________________________________
c 
c restarts              : 114
c conflicts             : 2261           (21 /sec)
c decisions             : 26424          (241 /sec)
c propagations          : 2705923        (24723 /sec)
c inspects              : 9347470        (85404 /sec)
c CPU time              : 109.45 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.87 0.94 0.90 2/54 15141
Raw data (stat): 15141 (runsolver) R 15140 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483520603 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.89 0.94 0.90 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 8048 0 0 0 968 30 0 0 25 0 1 0 483520603 20676608 4305 4294967295 134512640 134672761 3221224544 3221222992 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5048 4305 603 41 0 5007 0
vsize: 20192
[startup+20.0016 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 16975 0 0 0 1936 61 0 0 25 0 1 0 483520603 26857472 5594 4294967295 134512640 134672761 3221224544 3221222992 134643524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6557 5594 603 41 0 6516 0
vsize: 26228
[startup+30.0014 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 31899 0 0 0 2881 116 0 0 25 0 1 0 483520603 34082816 6846 4294967295 134512640 134672761 3221224544 3221222880 134605433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8321 6846 603 41 0 8280 0
vsize: 33284
[startup+40.0013 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 52127 0 0 0 3806 190 0 0 25 0 1 0 483520603 33165312 6745 4294967295 134512640 134672761 3221224544 3221222808 1075730078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8097 6745 603 41 0 8056 0
vsize: 32388
[startup+50.0019 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 72217 0 0 0 4732 264 0 0 25 0 1 0 483520603 34623488 7064 4294967295 134512640 134672761 3221224544 3221222804 1075347060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8453 7064 603 41 0 8412 0
vsize: 33812
[startup+60.0028 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 92939 0 0 0 5655 340 0 0 25 0 1 0 483520603 33898496 7000 4294967295 134512640 134672761 3221224544 3221222808 1075730078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8276 7000 603 41 0 8235 0
vsize: 33104
[startup+70.0036 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 114916 0 0 0 6578 416 0 0 25 0 1 0 483520603 33415168 6942 4294967295 134512640 134672761 3221224544 3221222856 134644405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8158 6942 603 41 0 8117 0
vsize: 32632
[startup+80.0032 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 135945 0 0 0 7503 491 0 0 25 0 1 0 483520603 33611776 7021 4294967295 134512640 134672761 3221224544 3221222988 1075278846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8206 7021 603 41 0 8165 0
vsize: 32824
[startup+90.0029 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 155526 0 0 0 8430 564 0 0 25 0 1 0 483520603 33505280 7058 4294967295 134512640 134672761 3221224544 3221222808 1075730078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8180 7058 603 41 0 8139 0
vsize: 32720
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 176008 0 0 0 9355 638 0 0 25 0 1 0 483520603 33497088 7098 4294967295 134512640 134672761 3221224544 3221222808 1075730078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8178 7098 603 41 0 8137 0
vsize: 32712
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 196340 0 0 0 10281 711 0 0 25 0 1 0 483520603 30371840 6286 4294967295 134512640 134672761 3221224544 3221222816 134565480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7415 6286 603 41 0 7374 0
vsize: 29660
[startup+117.084 s]
Raw data (loadavg): 0.98 0.95 0.91 1/53 15141
Raw data (stat): 15141 (minisat+) R 15140 24215 24214 0 -1 0 196340 0 0 0 10281 711 0 0 25 0 1 0 483520603 30371840 6286 4294967295 134512640 134672761 3221224544 3221222816 134565480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7415 6286 603 41 0 7374 0
vsize: 0

Child status: 30
Real time (s): 117.083
CPU time (s): 117.004
CPU user time (s): 109.472
CPU system time (s): 7.53185
CPU usage (%): 99.9323
Max. virtual memory (Kb): 33812
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1843200
#### END VERIFIER DATA ####