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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM	4f5f6e30a602f3968daa9ca41c7da043
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2058
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	9334
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1024
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	9334
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05284
Number of variables	133
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 14069

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-20 22:49:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19719 boxname=wulflinc5 idbench=1517 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f5f6e30a602f3968daa9ca41c7da043  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos5.opb
IDLAUNCH: 19719
/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:        574200 kB
Buffers:         38804 kB
Cached:         396572 kB
SwapCached:       2272 kB
Active:         219600 kB
Inactive:       220928 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        573948 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14368 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:09:59 (client local time) WITH STATUS 10 IN 1200.11 SECONDS
stats: 19719 7 1200.11 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    7
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    7
c ---[  63]---> BDD-cost:    7
c ---[  62]---> Sorter-cost:  382     Base:
c ---[  61]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  868     Base: 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  898     Base: 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1011     Base: 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  216     Base:
c ---[  50]---> Sorter-cost:  856     Base: 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1043     Base: 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  488     Base: 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  351     Base: 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  345     Base: 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  810     Base: 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  130     Base:
c ---[   1]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   25061    60133 |    7518       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/16432          
c   -- var.elim.:  2000/16432          
c   -- var.elim.:  3000/16432          
c   -- var.elim.:  4000/16432          
c   -- var.elim.:  5000/16432          
c   -- var.elim.:  6000/16432          
c   -- var.elim.:  7000/16432          
c   -- var.elim.:  8000/16432          
c   -- var.elim.:  9000/16432          
c   -- var.elim.:  10000/16432          
c   -- var.elim.:  11000/16432          
c   -- var.elim.:  12000/16432          
c   -- var.elim.:  13000/16432          
c   -- var.elim.:  14000/16432          
c   -- var.elim.:  15000/16432          
c   -- var.elim.:  16000/16432          
c   -- var.elim.:  16432/16432          
c   -- var.elim.:  1000/7680          
c   -- var.elim.:  2000/7680          
c   -- var.elim.:  3000/7680          
c   -- var.elim.:  4000/7680          
c   -- var.elim.:  5000/7680          
c   -- var.elim.:  6000/7680          
c   -- var.elim.:  7000/7680          
c   -- var.elim.:  7680/7680          
c   -- var.elim.:  1000/1433          
c   -- var.elim.:  1433/1433          
c   -- var.elim.:  672/672          
c   -- subsuming                       
c   -- var.elim.:  1000/6793          
c   -- var.elim.:  2000/6793          
c   -- var.elim.:  3000/6793          
c   -- var.elim.:  4000/6793          
c   -- var.elim.:  5000/6793          
c   -- var.elim.:  6000/6793          
c   -- var.elim.:  6793/6793          
c   -- var.elim.:  1000/3359          
c   -- var.elim.:  2000/3359          
c   -- var.elim.:  3000/3359          
c   -- var.elim.:  3359/3359          
c   -- subsuming                       
c   -- var.elim.:  1000/1647          
c   -- var.elim.:  1647/1647          
c   -- var.elim.:  294/294          
c |         0 |   16462    84306 |      --       0       --      -- |     --   | -8596/24254
c |         0 |   16462    84306 |    6584       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.25935 s)
c ==============================================================================
c [1mFound solution: 7890[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2068     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         2 |   21228    95514 |    6368       2       35    17.5 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2460          
c   -- var.elim.:  2000/2460          
c   -- var.elim.:  2460/2460          
c   -- var.elim.:  1000/1262          
c   -- var.elim.:  1262/1262          
c   -- subsuming                       
c   -- var.elim.:  396/396          
c   -- var.elim.:  274/274          
c   -- subsuming                       
c   -- var.elim.:  111/111          
c |         2 |   20492    98144 |      --       2       --      -- |     --   | -736/2631
c |         2 |   20492    98144 |    8196       2       35    17.5 |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.98024 s)
c ==============================================================================
c [1mFound solution: 4663[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        17 |   21058    99688 |    6317      17       90     5.3 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  845/845          
c   -- var.elim.:  432/432          
c   -- subsuming                       
c   -- var.elim.:  330/330          
c |        17 |   20656    99317 |      --      17       --      -- |     --   | -402/-370
c |        17 |   20656    99317 |    8262      17       90     5.3 |  0.000 % |
c ==============================================================================
c (current CPU-time: 5.41418 s)
c ==============================================================================
c [1mFound solution: 3380[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        78 |   21095   100557 |    6328      78      927    11.9 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  744/744          
c   -- var.elim.:  402/402          
c |        78 |   20766   100297 |      --      78       --      -- |     --   | -329/-259
c |        78 |   20766   100297 |    8306      78      927    11.9 |  0.000 % |
c ==============================================================================
c (current CPU-time: 5.83111 s)
c ==============================================================================
c [1mFound solution: 2616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       152 |   21083   101205 |    6324     152     1457     9.6 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  554/554          
c   -- var.elim.:  294/294          
c |       152 |   20833   100946 |      --     152       --      -- |     --   | -250/-258
c |       152 |   20833   100946 |    8333     152     1457     9.6 |  0.000 % |
c |       254 |   20833   100946 |    9166     254     3835    15.1 |  1.010 % |
c ==============================================================================
c (current CPU-time: 6.41702 s)
c ==============================================================================
c [1mFound solution: 2614[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       348 |   20887   101127 |    6266     348     5660    16.3 |  1.010 % |
c   -- subsuming                       
c   -- var.elim.:  325/325          
c   -- var.elim.:  89/89          
c |       348 |   20861   101265 |      --     348       --      -- |     --   | -26/139
c |       348 |   20861   101265 |    8344     348     5660    16.3 |  1.010 % |
c |       449 |   20861   101265 |    9178     449     8285    18.5 |  1.021 % |
c ==============================================================================
c (current CPU-time: 6.82996 s)
c ==============================================================================
c [1mFound solution: 2613[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       491 |   20905   101419 |    6271     491     9402    19.1 |  1.021 % |
c   -- subsuming                       
c   -- var.elim.:  107/107          
c   -- var.elim.:  79/79          
c |       491 |   20883   101606 |      --     491       --      -- |     --   | -22/188
c |       491 |   20883   101606 |    8353     491     9402    19.1 |  1.021 % |
c |       593 |   20883   101606 |    9188     593    11801    19.9 |  1.033 % |
c ==============================================================================
c (current CPU-time: 7.2409 s)
c ==============================================================================
c [1mFound solution: 2611[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       673 |   20926   101750 |    6277     673    13340    19.8 |  1.033 % |
c   -- subsuming                       
c   -- var.elim.:  98/98          
c   -- var.elim.:  71/71          
c |       673 |   20905   101923 |      --     673       --      -- |     --   | -21/174
c |       673 |   20905   101923 |    8362     673    13340    19.8 |  1.033 % |
c ==============================================================================
c (current CPU-time: 7.57385 s)
c ==============================================================================
c [1mFound solution: 2610[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       743 |   20948   102059 |    6284     743    14159    19.1 |  1.033 % |
c   -- subsuming                       
c   -- var.elim.:  90/90          
c   -- var.elim.:  63/63          
c |       743 |   20927   102216 |      --     743       --      -- |     --   | -21/158
c |       743 |   20927   102216 |    8370     743    14159    19.1 |  1.033 % |
c |       844 |   20927   102216 |    9207     844    17681    20.9 |  1.057 % |
c ==============================================================================
c (current CPU-time: 7.99078 s)
c ==============================================================================
c [1mFound solution: 2609[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       878 |   20973   102373 |    6291     878    18048    20.6 |  1.057 % |
c   -- subsuming                       
c   -- var.elim.:  108/108          
c   -- var.elim.:  80/80          
c |       878 |   20951   102528 |      --     878       --      -- |     --   | -22/156
c |       878 |   20951   102528 |    8380     878    18048    20.6 |  1.057 % |
c ==============================================================================
c (current CPU-time: 8.27974 s)
c ==============================================================================
c [1mFound solution: 2604[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       886 |   20997   102678 |    6299     886    18181    20.5 |  1.057 % |
c   -- subsuming                       
c   -- var.elim.:  101/101          
c   -- var.elim.:  73/73          
c |       886 |   20975   102815 |      --     886       --      -- |     --   | -22/138
c |       886 |   20975   102815 |    8390     886    18181    20.5 |  1.057 % |
c ==============================================================================
c (current CPU-time: 8.58669 s)
c ==============================================================================
c [1mFound solution: 2422[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 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 |   21107   103208 |    6332     927    18441    19.9 |  1.057 % |
c   -- subsuming                       
c   -- var.elim.:  238/238          
c   -- var.elim.:  142/142          
c |       927 |   21020   104142 |      --     927       --      -- |     --   | -87/935
c |       927 |   21020   104142 |    8408     927    18441    19.9 |  1.057 % |
c ==============================================================================
c (current CPU-time: 8.92664 s)
c ==============================================================================
c [1mFound solution: 2405[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1002 |   21125   104468 |    6337    1002    19398    19.4 |  1.057 % |
c   -- subsuming                       
c   -- var.elim.:  205/205          
c   -- var.elim.:  122/122          
c |      1002 |   21051   104595 |      --    1002       --      -- |     --   | -74/128
c |      1002 |   21051   104595 |    8420    1002    19398    19.4 |  1.057 % |
c |      1104 |   21051   104595 |    9262    1104    23647    21.4 |  1.103 % |
c ==============================================================================
c (current CPU-time: 9.50255 s)
c ==============================================================================
c [1mFound solution: 2326[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1243 |   21157   104927 |    6347    1243    28046    22.6 |  1.103 % |
c   -- subsuming                       
c   -- var.elim.:  205/205          
c   -- var.elim.:  126/126          
c |      1243 |   21076   104879 |      --    1243       --      -- |     --   | -81/-47
c |      1243 |   21076   104879 |    8430    1243    28046    22.6 |  1.103 % |
c ==============================================================================
c (current CPU-time: 9.81451 s)
c ==============================================================================
c [1mFound solution: 2325[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1269 |   21181   105204 |    6354    1269    29084    22.9 |  1.103 % |
c   -- subsuming                       
c   -- var.elim.:  198/198          
c   -- var.elim.:  121/121          
c |      1269 |   21101   105180 |      --    1269       --      -- |     --   | -80/-23
c |      1269 |   21101   105180 |    8440    1269    29084    22.9 |  1.103 % |
c ==============================================================================
c (current CPU-time: 10.1815 s)
c ==============================================================================
c [1mFound solution: 2324[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1324 |   21205   105496 |    6361    1324    30087    22.7 |  1.103 % |
c   -- subsuming                       
c   -- var.elim.:  190/190          
c   -- var.elim.:  114/114          
c |      1324 |   21126   105474 |      --    1324       --      -- |     --   | -79/-21
c |      1324 |   21126   105474 |    8450    1324    30087    22.7 |  1.103 % |
c |      1424 |   21126   105474 |    9295    1424    32631    22.9 |  1.138 % |
c |      1576 |   21126   105474 |   10224    1576    38251    24.3 |  1.138 % |
c ==============================================================================
c (current CPU-time: 10.8054 s)
c ==============================================================================
c [1mFound solution: 2194[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1691 |   21405   106261 |    6421    1691    42183    24.9 |  1.138 % |
c   -- subsuming                       
c   -- var.elim.:  478/478          
c   -- var.elim.:  244/244          
c |      1691 |   21167   105861 |      --    1691       --      -- |     --   | -238/-399
c |      1691 |   21167   105861 |    8466    1691    42183    24.9 |  1.138 % |
c |      1793 |   21167   105861 |    9313    1793    46441    25.9 |  1.148 % |
c ==============================================================================
c (current CPU-time: 11.3523 s)
c ==============================================================================
c [1mFound solution: 2193[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1846 |   21211   106004 |    6363    1846    47752    25.9 |  1.148 % |
c   -- subsuming                       
c   -- var.elim.:  276/276          
c   -- var.elim.:  68/68          
c |      1846 |   21190   106071 |      --    1846       --      -- |     --   | -21/68
c |      1846 |   21190   106071 |    8476    1846    47752    25.9 |  1.148 % |
c |      1948 |   21160   105847 |    9310    1941    50011    25.8 |  1.280 % |
c ==============================================================================
c (current CPU-time: 11.8192 s)
c ==============================================================================
c [1mFound solution: 2192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1984 |   21207   106001 |    6362    1977    51217    25.9 |  1.280 % |
c   -- subsuming                       
c   -- var.elim.:  265/265          
c   -- var.elim.:  74/74          
c |      1984 |   21185   106128 |      --    1977       --      -- |     --   | -22/128
c |      1984 |   21185   106128 |    8474    1970    51183    26.0 |  1.280 % |
c |      2085 |   21185   106128 |    9321    2071    53649    25.9 |  1.291 % |
c |      2236 |   21185   106128 |   10253    2222    60075    27.0 |  1.291 % |
c ==============================================================================
c (current CPU-time: 12.5121 s)
c ==============================================================================
c [1mFound solution: 2191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2333 |   21229   106267 |    6368    2319    61858    26.7 |  1.291 % |
c   -- subsuming                       
c   -- var.elim.:  91/91          
c   -- var.elim.:  64/64          
c |      2333 |   21209   106382 |      --    2319       --      -- |     --   | -20/116
c |      2333 |   21209   106382 |    8483    2319    61858    26.7 |  1.291 % |
c |      2433 |   21209   106382 |    9331    2419    66107    27.3 |  1.303 % |
c ==============================================================================
c (current CPU-time: 13.156 s)
c ==============================================================================
c [1mFound solution: 2190[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2557 |   21260   106556 |    6377    2543    71519    28.1 |  1.303 % |
c   -- subsuming                       
c   -- var.elim.:  119/119          
c   -- var.elim.:  86/86          
c |      2557 |   21234   106669 |      --    2543       --      -- |     --   | -26/114
c |      2557 |   21234   106669 |    8493    2543    71519    28.1 |  1.303 % |
c |      2658 |   21234   106669 |    9342    2644    75239    28.5 |  1.315 % |
c |      2808 |   21234   106669 |   10277    2794    80964    29.0 |  1.315 % |
c |      3033 |   21234   106669 |   11304    3019    93661    31.0 |  1.315 % |
c ==============================================================================
c (current CPU-time: 14.0999 s)
c ==============================================================================
c [1mFound solution: 2188[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3061 |   21277   106798 |    6383    3047    94856    31.1 |  1.315 % |
c   -- subsuming                       
c   -- var.elim.:  82/82          
c   -- var.elim.:  56/56          
c |      3061 |   21258   106915 |      --    3047       --      -- |     --   | -19/118
c |      3061 |   21258   106915 |    8503    3047    94856    31.1 |  1.315 % |
c |      3161 |   21258   106915 |    9353    3147   100493    31.9 |  1.326 % |
c |      3312 |   21258   106915 |   10288    3298   118677    36.0 |  1.326 % |
c ==============================================================================
c (current CPU-time: 14.7208 s)
c ==============================================================================
c [1mFound solution: 2187[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3350 |   21305   107068 |    6391    3336   119249    35.7 |  1.326 % |
c   -- subsuming                       
c   -- var.elim.:  102/102          
c   -- var.elim.:  73/73          
c |      3350 |   21283   107189 |      --    3336       --      -- |     --   | -22/122
c |      3350 |   21283   107189 |    8513    3336   119249    35.7 |  1.326 % |
c |      3450 |   21283   107189 |    9364    3436   127707    37.2 |  1.338 % |
c ==============================================================================
c (current CPU-time: 15.2457 s)
c ==============================================================================
c [1mFound solution: 2186[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3507 |   21329   107332 |    6398    3493   130033    37.2 |  1.338 % |
c   -- subsuming                       
c   -- var.elim.:  93/93          
c   -- var.elim.:  65/65          
c |      3507 |   21308   107455 |      --    3493       --      -- |     --   | -21/124
c |      3507 |   21308   107455 |    8523    3493   130033    37.2 |  1.338 % |
c |      3607 |   21308   107455 |    9375    3593   132442    36.9 |  1.349 % |
c ==============================================================================
c (current CPU-time: 15.7616 s)
c ==============================================================================
c [1mFound solution: 2184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3686 |   21348   107485 |    6404    3649   133965    36.7 |  1.349 % |
c   -- subsuming                       
c   -- var.elim.:  250/250          
c   -- var.elim.:  72/72          
c |      3686 |   21326   107613 |      --    3649       --      -- |     --   | -22/129
c |      3686 |   21326   107613 |    8530    3649   133965    36.7 |  1.349 % |
c ==============================================================================
c (current CPU-time: 16.0976 s)
c ==============================================================================
c [1mFound solution: 2182[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3729 |   21375   107781 |    6412    3692   136096    36.9 |  1.349 % |
c   -- subsuming                       
c   -- var.elim.:  115/115          
c   -- var.elim.:  84/84          
c |      3729 |   21351   107885 |      --    3692       --      -- |     --   | -24/105
c |      3729 |   21351   107885 |    8540    3692   136096    36.9 |  1.349 % |
c |      3829 |   21351   107885 |    9394    3792   137570    36.3 |  1.432 % |
c |      3979 |   21351   107885 |   10333    3942   151505    38.4 |  1.432 % |
c ==============================================================================
c (current CPU-time: 16.7834 s)
c ==============================================================================
c [1mFound solution: 2180[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4029 |   21397   108035 |    6419    3992   153523    38.5 |  1.432 % |
c   -- subsuming                       
c   -- var.elim.:  100/100          
c   -- var.elim.:  72/72          
c |      4029 |   21376   108145 |      --    3992       --      -- |     --   | -21/111
c |      4029 |   21376   108145 |    8550    3992   153523    38.5 |  1.432 % |
c ==============================================================================
c (current CPU-time: 17.1234 s)
c ==============================================================================
c [1mFound solution: 2178[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4049 |   21420   108282 |    6425    4012   154425    38.5 |  1.432 % |
c   -- subsuming                       
c   -- var.elim.:  89/89          
c   -- var.elim.:  63/63          
c |      4049 |   21401   108396 |      --    4012       --      -- |     --   | -19/115
c |      4049 |   21401   108396 |    8560    4012   154425    38.5 |  1.432 % |
c ==============================================================================
c (current CPU-time: 17.4683 s)
c ==============================================================================
c [1mFound solution: 2177[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4086 |   21445   108533 |    6433    4049   157185    38.8 |  1.432 % |
c   -- subsuming                       
c   -- var.elim.:  89/89          
c   -- var.elim.:  63/63          
c |      4086 |   21426   108647 |      --    4049       --      -- |     --   | -19/115
c |      4086 |   21426   108647 |    8570    4049   157185    38.8 |  1.432 % |
c ==============================================================================
c (current CPU-time: 17.8463 s)
c ==============================================================================
c [1mFound solution: 2176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4124 |   21449   108537 |    6434    4085   158346    38.8 |  1.432 % |
c   -- subsuming                       
c   -- var.elim.:  479/479          
c   -- var.elim.:  75/75          
c |      4124 |   21426   108639 |      --    4085       --      -- |     --   | -23/103
c |      4124 |   21426   108639 |    8570    4085   158346    38.8 |  1.432 % |
c |      4225 |   21426   108639 |    9427    4186   163578    39.1 |  1.598 % |
c |      4375 |   21426   108639 |   10370    4336   168313    38.8 |  1.598 % |
c |      4600 |   21423   108621 |   11405    4535   176956    39.0 |  1.610 % |
c |      4938 |   21423   108621 |   12546    4873   195785    40.2 |  1.610 % |
c |      5445 |   21423   108621 |   13800    5380   234448    43.6 |  1.610 % |
c |      6204 |   21423   108621 |   15180    6139   268069    43.7 |  1.610 % |
c ==============================================================================
c (current CPU-time: 20.6529 s)
c ==============================================================================
c [1mFound solution: 2067[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6426 |   21467   108765 |    6440    6361   279418    43.9 |  1.610 % |
c   -- subsuming                       
c   -- var.elim.:  211/211          
c   -- var.elim.:  69/69          
c |      6426 |   21448   108872 |      --    6361       --      -- |     --   | -19/108
c |      6426 |   21448   108872 |    8579    6361   279418    43.9 |  1.610 % |
c |      6526 |   21448   108872 |    9437    6461   282053    43.7 |  1.621 % |
c |      6676 |   21446   108854 |   10379    6610   291356    44.1 |  1.633 % |
c |      6901 |   21446   108854 |   11417    6835   303513    44.4 |  1.633 % |
c |      7240 |   21446   108854 |   12559    7174   329595    45.9 |  1.633 % |
c |      7746 |   21446   108854 |   13815    7680   371940    48.4 |  1.633 % |
c |      8506 |   21446   108854 |   15197    8440   481408    57.0 |  1.633 % |
c ==============================================================================
c (current CPU-time: 24.6812 s)
c ==============================================================================
c [1mFound solution: 2066[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9149 |   21482   108945 |    6444    9083   536417    59.1 |  1.633 % |
c   -- subsuming                       
c   -- var.elim.:  208/208          
c   -- var.elim.:  30/30          
c |      9149 |   21468   109060 |      --    9083       --      -- |     --   | -14/116
c |      9149 |   21468   109060 |    8587    9075   536319    59.1 |  1.633 % |
c |      9249 |   21468   109060 |    9445    6150   392465    63.8 |  1.645 % |
c |      9400 |   21468   109060 |   10390    6301   413561    65.6 |  1.645 % |
c |      9625 |   21468   109060 |   11429    6526   424926    65.1 |  1.645 % |
c |      9962 |   21468   109060 |   12572    6863   440125    64.1 |  1.645 % |
c |     10469 |   21468   109060 |   13829    7370   491898    66.7 |  1.645 % |
c |     11229 |   21468   109060 |   15212    8130   535679    65.9 |  1.645 % |
c |     12369 |   21468   109060 |   16734    9270   675376    72.9 |  1.645 % |
c ==============================================================================
c (current CPU-time: 30.4344 s)
c ==============================================================================
c [1mFound solution: 2064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13586 |   21513   109205 |    6453   10487   856088    81.6 |  1.645 % |
c   -- subsuming                       
c   -- var.elim.:  97/97          
c   -- var.elim.:  68/68          
c |     13586 |   21490   109316 |      --   10487       --      -- |     --   | -23/112
c |     13586 |   21490   109316 |    8596   10487   856088    81.6 |  1.645 % |
c |     13686 |   21490   109316 |    9455    7092   580678    81.9 |  1.656 % |
c |     13836 |   21490   109316 |   10401    7242   591218    81.6 |  1.656 % |
c |     14061 |   21490   109316 |   11441    7467   614094    82.2 |  1.656 % |
c ==============================================================================
c (current CPU-time: 32.0441 s)
c ==============================================================================
c [1mFound solution: 2063[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14378 |   21531   109444 |    6459    7784   632348    81.2 |  1.656 % |
c   -- subsuming                       
c   -- var.elim.:  84/84          
c   -- var.elim.:  58/58          
c |     14378 |   21511   109542 |      --    7784       --      -- |     --   | -20/99
c |     14378 |   21511   109542 |    8604    7784   632348    81.2 |  1.656 % |
c |     14478 |   21511   109542 |    9464    7884   638899    81.0 |  1.668 % |
c |     14628 |   21511   109542 |   10411    8034   655167    81.5 |  1.668 % |
c |     14853 |   21511   109542 |   11452    8259   675557    81.8 |  1.668 % |
c |     15190 |   21511   109542 |   12597    8596   714123    83.1 |  1.668 % |
c ==============================================================================
c (current CPU-time: 33.6709 s)
c ==============================================================================
c [1mFound solution: 2062[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15267 |   21559   109705 |    6467    8673   728172    84.0 |  1.668 % |
c   -- subsuming                       
c   -- var.elim.:  112/112          
c   -- var.elim.:  80/80          
c |     15267 |   21533   109801 |      --    8673       --      -- |     --   | -26/97
c |     15267 |   21533   109801 |    8613    8673   728172    84.0 |  1.668 % |
c ==============================================================================
c (current CPU-time: 34.1118 s)
c ==============================================================================
c [1mFound solution: 2060[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15318 |   21573   109919 |    6471    8724   735237    84.3 |  1.668 % |
c   -- subsuming                       
c   -- var.elim.:  75/75          
c   -- var.elim.:  50/50          
c |     15318 |   21554   110019 |      --    8724       --      -- |     --   | -19/101
c |     15318 |   21554   110019 |    8621    8724   735237    84.3 |  1.668 % |
c ==============================================================================
c (current CPU-time: 34.5048 s)
c ==============================================================================
c [1mFound solution: 2058[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15368 |   21597   110151 |    6479    8774   741190    84.5 |  1.668 % |
c   -- subsuming                       
c   -- var.elim.:  86/86          
c   -- var.elim.:  59/59          
c |     15368 |   21576   110257 |      --    8774       --      -- |     --   | -21/107
c |     15368 |   21576   110257 |    8630    8774   741190    84.5 |  1.668 % |
c |     15471 |   21576   110257 |    9493    5953   497932    83.6 |  1.702 % |
c ==============================================================================
c (current CPU-time: 35.0747 s)
c ==============================================================================
c [1mFound solution: 2056[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15507 |   21622   110403 |    6486    5989   502113    83.8 |  1.702 % |
c   -- subsuming                       
c   -- var.elim.:  97/97          
c   -- var.elim.:  68/68          
c |     15507 |   21599   110515 |      --    5989       --      -- |     --   | -23/113
c |     15507 |   21599   110515 |    8639    5989   502113    83.8 |  1.702 % |
c |     15607 |   21599   110515 |    9503    6089   512259    84.1 |  1.714 % |
c |     15759 |   21599   110515 |   10453    6241   520533    83.4 |  1.714 % |
c |     15984 |   21599   110515 |   11499    6466   532258    82.3 |  1.714 % |
c |     16322 |   21540   109750 |   12614    6797   550981    81.1 |  1.880 % |
c |     16828 |   21540   109750 |   13876    7303   583202    79.9 |  1.880 % |
c |     17588 |   21540   109750 |   15263    8063   606309    75.2 |  1.880 % |
c |     18729 |   21540   109750 |   16790    9204   739895    80.4 |  1.880 % |
c ==============================================================================
c (current CPU-time: 40.3119 s)
c ==============================================================================
c [1mFound solution: 2055[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19792 |   21578   109863 |    6473   10267   871264    84.9 |  1.880 % |
c   -- subsuming                       
c   -- var.elim.:  483/483          
c   -- var.elim.:  312/312          
c   -- var.elim.:  192/192          
c   -- var.elim.:  209/209          
c |     19792 |   21542   110496 |      --   10267       --      -- |     --   | -36/634
c |     19792 |   21542   110496 |    8616    9932   815669    82.1 |  1.880 % |
c |     19892 |   21542   110496 |    9478    6722   446746    66.5 |  1.895 % |
c |     20043 |   21542   110496 |   10426    6873   467323    68.0 |  1.896 % |
c ==============================================================================
c (current CPU-time: 41.4467 s)
c ==============================================================================
c [1mFound solution: 2054[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20083 |   21589   110657 |    6476    6913   472763    68.4 |  1.896 % |
c   -- subsuming                       
c   -- var.elim.:  337/337          
c   -- var.elim.:  80/80          
c |     20083 |   21564   110534 |      --    6913       --      -- |     --   | -25/-122
c |     20083 |   21564   110534 |    8625    6913   472763    68.4 |  1.896 % |
c |     20185 |   21564   110534 |    9488    7015   481926    68.7 |  1.907 % |
c |     20335 |   21564   110534 |   10436    7165   499031    69.6 |  1.907 % |
c |     20561 |   21564   110534 |   11480    7391   522041    70.6 |  1.907 % |
c |     20898 |   21564   110534 |   12628    7728   565851    73.2 |  1.907 % |
c |     21404 |   21564   110534 |   13891    8234   605915    73.6 |  1.907 % |
c ==============================================================================
c (current CPU-time: 44.4362 s)
c ==============================================================================
c [1mFound solution: 2052[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     21871 |   21608   110677 |    6482    8701   654598    75.2 |  1.907 % |
c   -- subsuming                       
c   -- var.elim.:  96/96          
c   -- var.elim.:  68/68          
c |     21871 |   21586   110771 |      --    8701       --      -- |     --   | -22/95
c |     21871 |   21586   110771 |    8634    8701   654598    75.2 |  1.907 % |
c |     21972 |   21586   110771 |    9497    8802   657043    74.6 |  1.918 % |
c |     22122 |   21586   110771 |   10447    8952   660186    73.7 |  1.918 % |
c |     22347 |   21586   110771 |   11492    9177   673576    73.4 |  1.918 % |
c ==============================================================================
c (current CPU-time: 45.734 s)
c ==============================================================================
c [1mFound solution: 2051[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     22567 |   21628   110909 |    6488    9397   698359    74.3 |  1.918 % |
c   -- subsuming                       
c   -- var.elim.:  93/93          
c   -- var.elim.:  67/67          
c |     22567 |   21608   111007 |      --    9397       --      -- |     --   | -20/99
c |     22567 |   21608   111007 |    8643    9397   698359    74.3 |  1.918 % |
c |     22668 |   21608   111007 |    9507    6366   452973    71.2 |  1.930 % |
c |     22818 |   21608   111007 |   10458    6516   467268    71.7 |  1.930 % |
c ==============================================================================
c (current CPU-time: 46.8409 s)
c ==============================================================================
c [1mFound solution: 2050[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23014 |   21650   111137 |    6494    6712   477752    71.2 |  1.930 % |
c   -- subsuming                       
c   -- var.elim.:  85/85          
c   -- var.elim.:  59/59          
c |     23014 |   21630   111235 |      --    6712       --      -- |     --   | -20/99
c |     23014 |   21630   111235 |    8652    6712   477752    71.2 |  1.930 % |
c |     23114 |   21630   111235 |    9517    6812   481772    70.7 |  1.941 % |
c |     23264 |   21630   111235 |   10468    6962   505769    72.6 |  1.941 % |
c |     23490 |   21630   111235 |   11515    7188   530114    73.7 |  1.941 % |
c ==============================================================================
c (current CPU-time: 48.1157 s)
c ==============================================================================
c [1mFound solution: 2049[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23654 |   21672   111365 |    6501    7352   561658    76.4 |  1.941 % |
c   -- subsuming                       
c   -- var.elim.:  85/85          
c   -- var.elim.:  59/59          
c |     23654 |   21652   111463 |      --    7352       --      -- |     --   | -20/99
c |     23654 |   21652   111463 |    8660    7352   561658    76.4 |  1.941 % |
c |     23754 |   21652   111463 |    9526    7452   572133    76.8 |  1.953 % |
c |     23904 |   21652   111463 |   10479    7602   579952    76.3 |  1.953 % |
c |     24131 |   21652   111463 |   11527    7829   586915    75.0 |  1.953 % |
c ==============================================================================
c (current CPU-time: 49.3235 s)
c ==============================================================================
c [1mFound solution: 2048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24173 |   21697   111607 |    6509    7871   589127    74.8 |  1.953 % |
c   -- subsuming                       
c   -- var.elim.:  96/96          
c   -- var.elim.:  68/68          
c |     24173 |   21675   111710 |      --    7871       --      -- |     --   | -22/104
c |     24173 |   21675   111710 |    8670    7871   589127    74.8 |  1.953 % |
c |     24273 |   21675   111710 |    9537    7971   596556    74.8 |  1.964 % |
c |     24423 |   21669   111656 |   10487    7998   583359    72.9 |  2.000 % |
c |     24648 |   21669   111656 |   11536    8223   608740    74.0 |  2.000 % |
c |     24988 |   21669   111656 |   12690    8563   629496    73.5 |  2.000 % |
c |     25494 |   21669   111656 |   13959    9069   649298    71.6 |  2.000 % |
c |     26257 |   21669   111656 |   15355    9832   702068    71.4 |  2.000 % |
c |     27396 |   21669   111656 |   16890   10971   827534    75.4 |  2.000 % |
c |     29105 |   21669   111656 |   18579   12680  1039341    82.0 |  2.000 % |
c |     31667 |   21669   111656 |   20437   15242  1150086    75.5 |  2.000 % |
c |     35512 |   21663   111605 |   22475   19063  1736928    91.1 |  2.036 % |
c |     41279 |   21663   111605 |   24722   24830  2195789    88.4 |  2.036 % |
c |     49928 |   21663   111605 |   27195   22421  2156019    96.2 |  2.036 % |
c |     62902 |   21533   109974 |   29735   22156  2328321   105.1 |  2.619 % |
c ==============================================================================
c (current CPU-time: 101.408 s)
c ==============================================================================
c [1mFound solution: 2038[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     65743 |   21652   110335 |    6495   24997  2607193   104.3 |  2.619 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1489          
c   -- var.elim.:  1489/1489          
c   -- var.elim.:  367/367          
c   -- var.elim.:  288/288          
c   -- var.elim.:  240/240          
c   -- subsuming                       
c   -- var.elim.:  282/282          
c |     65743 |   21519   111373 |      --   24997       --      -- |     --   | -133/1039
c |     65743 |   21519   111373 |    8607   23495  2184110    93.0 |  2.619 % |
c |     65844 |   21519   111373 |    9468    8895   542023    60.9 |  2.673 % |
c |     65995 |   21519   111373 |   10415    9046   546868    60.5 |  2.673 % |
c |     66221 |   21519   111373 |   11456    9272   558977    60.3 |  2.673 % |
c |     66560 |   21519   111373 |   12602    9611   576272    60.0 |  2.673 % |
c |     67066 |   21519   111373 |   13862   10117   610169    60.3 |  2.673 % |
c |     67826 |   21519   111373 |   15248   10877   701957    64.5 |  2.673 % |
c |     68965 |   21503   111279 |   16761   12015   786770    65.5 |  2.769 % |
c |     70673 |   21503   111279 |   18437   13723   913903    66.6 |  2.769 % |
c |     73235 |   21503   111279 |   20281   16285  1170515    71.9 |  2.769 % |
c |     77079 |   21503   111279 |   22309   20129  1552102    77.1 |  2.769 % |
c |     82848 |   21487   111185 |   24521   16280  1806942   111.0 |  2.864 % |
c |     91497 |   21487   111185 |   26974   24929  3324634   133.4 |  2.864 % |
c |    104472 |   21487   111185 |   29671   24477  3320422   135.7 |  2.864 % |
c |    123935 |   21487   111185 |   32638   24536  5020092   204.6 |  2.864 % |
c ==============================================================================
c (current CPU-time: 232.258 s)
c ==============================================================================
c [1mFound solution: 2037[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    141554 |   21539   111357 |    6461   19338  6041606   312.4 |  2.864 % |
c   -- subsuming                       
c   -- var.elim.:  408/408          
c   -- var.elim.:  83/83          
c |    141554 |   21510   112134 |      --   19338       --      -- |     --   | -29/778
c |    141554 |   21510   112134 |    8604   19338  6041606   312.4 |  2.864 % |
c |    141654 |   21510   112134 |    9464    8695  1823350   209.7 |  2.876 % |
c |    141806 |   21510   112134 |   10410    8847  1832490   207.1 |  2.876 % |
c |    142032 |   21510   112134 |   11451    9073  1842018   203.0 |  2.876 % |
c |    142369 |   21510   112134 |   12597    9410  1860560   197.7 |  2.876 % |
c |    142877 |   21510   112134 |   13856    9918  1884491   190.0 |  2.876 % |
c |    143636 |   21510   112134 |   15242   10677  1972713   184.8 |  2.876 % |
c |    144776 |   21510   112134 |   16766   11817  2066959   174.9 |  2.876 % |
c |    146485 |   21510   112134 |   18443   13526  2185449   161.6 |  2.876 % |
c |    149047 |   21510   112134 |   20287   16088  2387926   148.4 |  2.876 % |
c |    152891 |   21510   112134 |   22316   19932  2719981   136.5 |  2.876 % |
c ==============================================================================
c (current CPU-time: 255.62 s)
c ==============================================================================
c [1mFound solution: 2036[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    157984 |   21556   112247 |    6466   15475  1288293    83.2 |  2.876 % |
c   -- subsuming                       
c   -- var.elim.:  286/286          
c   -- var.elim.:  84/84          
c |    157984 |   21527   112923 |      --   15475       --      -- |     --   | -29/677
c |    157984 |   21527   112923 |    8610   15475  1288293    83.2 |  2.876 % |
c |    158085 |   21527   112923 |    9471    6979   549365    78.7 |  2.923 % |
c |    158235 |   21527   112923 |   10419    7129   560369    78.6 |  2.923 % |
c |    158460 |   21527   112923 |   11460    7354   570660    77.6 |  2.923 % |
c |    158798 |   21527   112923 |   12607    7692   590760    76.8 |  2.923 % |
c |    159306 |   21527   112923 |   13867    8200   634785    77.4 |  2.923 % |
c |    160065 |   21527   112923 |   15254    8959   702784    78.4 |  2.923 % |
c |    161204 |   21527   112923 |   16780   10098   837874    83.0 |  2.923 % |
c |    162912 |   21527   112923 |   18458   11806  1123346    95.2 |  2.923 % |
c |    165474 |   21527   112923 |   20303   14368  1406685    97.9 |  2.923 % |
c |    169318 |   21513   112811 |   22319   18195  2144879   117.9 |  3.006 % |
c |    175084 |   21509   112740 |   24547   23959  2869519   119.8 |  3.030 % |
c ==============================================================================
c (current CPU-time: 293.027 s)
c ==============================================================================
c [1mFound solution: 2035[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    183476 |   21365   110474 |    6409   21885  2432968   111.2 |  3.030 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1102          
c   -- var.elim.:  1102/1102          
c   -- var.elim.:  361/361          
c   -- var.elim.:  219/219          
c   -- var.elim.:  158/158          
c   -- subsuming                       
c   -- var.elim.:  26/26          
c   -- var.elim.:  31/31          
c |    183476 |   21163   110458 |      --   21885       --      -- |     --   | -202/-15
c |    183476 |   21163   110458 |    8465   17895  1618581    90.4 |  3.030 % |
c |    183576 |   21163   110458 |    9311    8054   593404    73.7 |  3.637 % |
c |    183726 |   21161   110450 |   10241    8203   598140    72.9 |  3.649 % |
c |    183951 |   21161   110450 |   11266    8428   616236    73.1 |  3.649 % |
c |    184288 |   21161   110450 |   12392    8765   627600    71.6 |  3.649 % |
c |    184794 |   21161   110450 |   13632    9271   673901    72.7 |  3.649 % |
c |    185554 |   21155   110405 |   14990   10030   748768    74.7 |  3.686 % |
c |    186695 |   21155   110405 |   16490   11171   875161    78.3 |  3.685 % |
c |    188403 |   21149   110362 |   18133   12870  1007573    78.3 |  3.722 % |
c |    190966 |   21138   110284 |   19936   15431  1234369    80.0 |  3.746 % |
c |    194811 |   21138   110284 |   21930   19276  1600379    83.0 |  3.746 % |
c ==============================================================================
c (current CPU-time: 316.436 s)
c ==============================================================================
c [1mFound solution: 2034[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    200511 |   21430   111043 |    6428   16260  2254689   138.7 |  3.746 % |
c   -- subsuming                       
c   -- var.elim.:  669/669          
c   -- var.elim.:  243/243          
c   -- var.elim.:  148/148          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  97/97          
c |    200511 |   21158   111010 |      --   16260       --      -- |     --   | -272/-32
c |    200511 |   21158   111010 |    8463   16250  2254244   138.7 |  3.746 % |
c |    200611 |   21158   111010 |    9309    7323  1338057   182.7 |  3.780 % |
c |    200761 |   21158   111010 |   10240    7473  1341802   179.6 |  3.780 % |
c |    200986 |   21158   111010 |   11264    7698  1355966   176.1 |  3.780 % |
c |    201324 |   21158   111010 |   12390    8036  1402296   174.5 |  3.780 % |
c |    201831 |   21158   111010 |   13630    8543  1433558   167.8 |  3.780 % |
c |    202591 |   21158   111010 |   14993    9303  1494263   160.6 |  3.780 % |
c |    203731 |   21142   110916 |   16479   10442  1576080   150.9 |  3.876 % |
c |    205443 |   21142   110916 |   18127   12154  1653508   136.0 |  3.876 % |
c |    208005 |   21135   110870 |   19934   14715  1826220   124.1 |  3.913 % |
c |    211849 |   21135   110870 |   21927   18559  2893977   155.9 |  3.913 % |
c |    217615 |   21127   110825 |   24111   15852  1826475   115.2 |  3.961 % |
c |    226265 |   21127   110825 |   26522   24502  3420841   139.6 |  3.961 % |
c ==============================================================================
c (current CPU-time: 355.226 s)
c ==============================================================================
c [1mFound solution: 2033[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    229591 |   21417   111567 |    6425   27822  3885266   139.6 |  3.961 % |
c   -- subsuming                       
c   -- var.elim.:  773/773          
c   -- var.elim.:  217/217          
c   -- var.elim.:  156/156          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  43/43          
c |    229591 |   21143   111483 |      --   27822       --      -- |     --   | -274/-83
c |    229591 |   21143   111483 |    8457   27822  3885266   139.6 |  3.961 % |
c |    229692 |   21143   111483 |    9302    6633   598097    90.2 |  3.983 % |
c |    229843 |   21143   111483 |   10233    6784   607849    89.6 |  3.983 % |
c |    230068 |   21143   111483 |   11256    7009   619258    88.4 |  3.983 % |
c |    230406 |   21143   111483 |   12382    7347   648419    88.3 |  3.983 % |
c |    230913 |   21143   111483 |   13620    7854   690859    88.0 |  3.983 % |
c |    231672 |   21143   111483 |   14982    8613   757349    87.9 |  3.983 % |
c |    232812 |   21143   111483 |   16480    9753   840656    86.2 |  3.983 % |
c ==============================================================================
c (current CPU-time: 362.077 s)
c ==============================================================================
c [1mFound solution: 2032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    233908 |   21440   112266 |    6431   10849   934865    86.2 |  3.983 % |
c   -- subsuming                       
c   -- var.elim.:  386/386          
c   -- var.elim.:  224/224          
c   -- var.elim.:  154/154          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  43/43          
c |    233908 |   21168   112187 |      --   10849       --      -- |     --   | -272/-78
c |    233908 |   21168   112187 |    8467   10849   934865    86.2 |  3.983 % |
c |    234008 |   21148   112037 |    9305    7331   447750    61.1 |  4.115 % |
c |    234158 |   21148   112037 |   10235    7481   461831    61.7 |  4.115 % |
c |    234383 |   21148   112037 |   11259    7706   470529    61.1 |  4.115 % |
c |    234721 |   21148   112037 |   12385    8044   496767    61.8 |  4.115 % |
c |    235228 |   21148   112037 |   13623    8551   526212    61.5 |  4.115 % |
c |    235987 |   21148   112037 |   14985    9310   570980    61.3 |  4.115 % |
c |    237126 |   21148   112037 |   16484   10449   665863    63.7 |  4.115 % |
c |    238835 |   21148   112037 |   18133   12158   799746    65.8 |  4.115 % |
c |    241399 |   21140   111989 |   19938   14717  1086240    73.8 |  4.163 % |
c |    245243 |   21140   111989 |   21932   18561  1431195    77.1 |  4.163 % |
c |    251009 |   21140   111989 |   24125   24327  3270750   134.4 |  4.163 % |
c |    259659 |   21135   111950 |   26532   23311  3568763   153.1 |  4.187 % |
c |    272633 |   21129   111904 |   29177   20789  2410107   115.9 |  4.224 % |
c |    292095 |   21129   111904 |   32094   23095  5063561   219.2 |  4.224 % |
c ==============================================================================
c (current CPU-time: 451.724 s)
c ==============================================================================
c [1mFound solution: 2031[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    296326 |   21423   112672 |    6426   27326  5506071   201.5 |  4.224 % |
c   -- subsuming                       
c   -- var.elim.:  952/952          
c   -- var.elim.:  223/223          
c   -- var.elim.:  155/155          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  42/42          
c |    296326 |   21151   112580 |      --   27326       --      -- |     --   | -272/-91
c |    296326 |   21151   112580 |    8460   27326  5506071   201.5 |  4.224 % |
c |    296426 |   21151   112580 |    9306    6425   465519    72.5 |  4.235 % |
c |    296578 |   21151   112580 |   10237    6577   471101    71.6 |  4.235 % |
c |    296804 |   21151   112580 |   11260    6803   478228    70.3 |  4.235 % |
c |    297141 |   21151   112580 |   12386    7140   492801    69.0 |  4.235 % |
c |    297647 |   21151   112580 |   13625    7646   527989    69.1 |  4.235 % |
c |    298408 |   21151   112580 |   14988    8407   593144    70.6 |  4.235 % |
c |    299547 |   21151   112580 |   16486    9546   658125    68.9 |  4.235 % |
c |    301255 |   21151   112580 |   18135   11254   822251    73.1 |  4.235 % |
c |    303819 |   21151   112580 |   19949   13818  1183721    85.7 |  4.235 % |
c |    307665 |   21151   112580 |   21944   17664  1571235    89.0 |  4.235 % |
c |    313432 |   21151   112580 |   24138   23431  2325338    99.2 |  4.235 % |
c |    322082 |   21151   112580 |   26552   21393  1925088    90.0 |  4.235 % |
c |    335057 |   21151   112580 |   29207   20279  3082152   152.0 |  4.235 % |
c ==============================================================================
c (current CPU-time: 515.271 s)
c ==============================================================================
c [1mFound solution: 2030[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    341382 |   21451   113381 |    6435   26604  3628718   136.4 |  4.235 % |
c   -- subsuming                       
c   -- var.elim.:  401/401          
c   -- var.elim.:  237/237          
c   -- var.elim.:  145/145          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  34/34          
c |    341382 |   21176   113161 |      --   26604       --      -- |     --   | -275/-219
c |    341382 |   21176   113161 |    8470   26604  3628718   136.4 |  4.235 % |
c |    341483 |   21176   113161 |    9317    6935   430878    62.1 |  4.246 % |
c |    341634 |   21176   113161 |   10249    7086   438519    61.9 |  4.246 % |
c |    341859 |   21176   113161 |   11274    7311   457677    62.6 |  4.246 % |
c |    342197 |   21176   113161 |   12401    7649   479881    62.7 |  4.246 % |
c |    342704 |   21176   113161 |   13641    8156   509897    62.5 |  4.246 % |
c |    343465 |   21176   113161 |   15005    8917   607027    68.1 |  4.246 % |
c |    344604 |   21176   113161 |   16506   10056   689062    68.5 |  4.246 % |
c |    346313 |   21176   113161 |   18157   11765   907728    77.2 |  4.246 % |
c |    348876 |   21176   113161 |   19972   14328  1234749    86.2 |  4.246 % |
c |    352721 |   21172   113123 |   21965   18172  1655837    91.1 |  4.270 % |
c |    358488 |   21172   113123 |   24162   23939  2562479   107.0 |  4.270 % |
c |    367140 |   21166   113077 |   26571   22691  3106576   136.9 |  4.307 % |
c |    380114 |   21166   113077 |   29228   21554  3220484   149.4 |  4.306 % |
c ==============================================================================
c (current CPU-time: 576.358 s)
c ==============================================================================
c [1mFound solution: 2022[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    385843 |   21467   113880 |    6440   27283  3852621   141.2 |  4.306 % |
c   -- subsuming                       
c   -- var.elim.:  746/746          
c   -- var.elim.:  239/239          
c   -- var.elim.:  137/137          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  24/24          
c |    385843 |   21191   113508 |      --   27283       --      -- |     --   | -276/-371
c |    385843 |   21191   113508 |    8476   27283  3852621   141.2 |  4.306 % |
c |    385943 |   21191   113508 |    9324    6950   501933    72.2 |  4.316 % |
c |    386093 |   21191   113508 |   10256    7100   508633    71.6 |  4.316 % |
c |    386323 |   21191   113508 |   11282    7330   519994    70.9 |  4.316 % |
c |    386660 |   21191   113508 |   12410    7667   570782    74.4 |  4.316 % |
c |    387166 |   21191   113508 |   13651    8173   599659    73.4 |  4.316 % |
c |    387925 |   21183   113460 |   15010    8931   651188    72.9 |  4.365 % |
c |    389065 |   21183   113460 |   16511   10071   749117    74.4 |  4.365 % |
c |    390773 |   21183   113460 |   18163   11779   879842    74.7 |  4.365 % |
c |    393336 |   21183   113460 |   19979   14342  1231478    85.9 |  4.365 % |
c |    397181 |   21183   113460 |   21977   18187  1839383   101.1 |  4.365 % |
c ==============================================================================
c (current CPU-time: 592.001 s)
c ==============================================================================
c [1mFound solution: 2006[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    397703 |   21484   114263 |    6445   18709  1908039   102.0 |  4.365 % |
c   -- subsuming                       
c   -- var.elim.:  537/537          
c   -- var.elim.:  237/237          
c   -- var.elim.:  125/125          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |    397703 |   21208   113741 |      --   18709       --      -- |     --   | -276/-521
c |    397703 |   21208   113741 |    8483   18709  1908039   102.0 |  4.365 % |
c |    397806 |   21208   113741 |    9331    8419   904017   107.4 |  4.376 % |
c |    397958 |   21208   113741 |   10264    8571   918215   107.1 |  4.376 % |
c |    398184 |   21208   113741 |   11291    8797   938089   106.6 |  4.376 % |
c |    398521 |   21208   113741 |   12420    9134   966556   105.8 |  4.376 % |
c |    399027 |   21208   113741 |   13662    9640   999743   103.7 |  4.376 % |
c |    399786 |   21208   113741 |   15028   10399  1074224   103.3 |  4.376 % |
c |    400926 |   21208   113741 |   16531   11539  1190457   103.2 |  4.376 % |
c |    402634 |   21204   113714 |   18181   13246  1385438   104.6 |  4.400 % |
c |    405197 |   21204   113714 |   19999   15809  1692749   107.1 |  4.400 % |
c |    409041 |   21187   113594 |   21981   19612  2395528   122.1 |  4.496 % |
c ==============================================================================
c (current CPU-time: 610.941 s)
c ==============================================================================
c [1mFound solution: 2005[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    410918 |   21486   114388 |    6445   21489  2603357   121.1 |  4.496 % |
c   -- subsuming                       
c   -- var.elim.:  776/776          
c   -- var.elim.:  241/241          
c   -- var.elim.:  127/127          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |    410918 |   21212   113873 |      --   21489       --      -- |     --   | -274/-514
c |    410918 |   21212   113873 |    8484   21489  2603357   121.1 |  4.496 % |
c |    411018 |   21212   113873 |    9333    6468   612328    94.7 |  4.507 % |
c |    411168 |   21212   113873 |   10266    6618   623637    94.2 |  4.507 % |
c |    411394 |   21212   113873 |   11293    6844   646600    94.5 |  4.507 % |
c |    411731 |   21212   113873 |   12422    7181   668742    93.1 |  4.507 % |
c |    412237 |   21212   113873 |   13664    7687   714791    93.0 |  4.507 % |
c |    412996 |   21212   113873 |   15031    8446   761795    90.2 |  4.507 % |
c |    414137 |   21212   113873 |   16534    9587   861043    89.8 |  4.507 % |
c |    415846 |   21212   113873 |   18187   11296  1073009    95.0 |  4.507 % |
c |    418408 |   21204   113825 |   19999   13857  1381773    99.7 |  4.555 % |
c |    422252 |   21204   113825 |   21999   17701  1817623   102.7 |  4.555 % |
c |    428020 |   21204   113825 |   24198   23469  2682439   114.3 |  4.555 % |
c |    436670 |   21204   113825 |   26618   21907  2169636    99.0 |  4.555 % |
c ==============================================================================
c (current CPU-time: 654.188 s)
c ==============================================================================
c [1mFound solution: 2004[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    443242 |   21502   114610 |    6450   28479  3632311   127.5 |  4.555 % |
c   -- subsuming                       
c   -- var.elim.:  520/520          
c   -- var.elim.:  225/225          
c   -- var.elim.:  125/125          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |    443242 |   21229   114094 |      --   28479       --      -- |     --   | -273/-515
c |    443242 |   21229   114094 |    8491   28479  3632311   127.5 |  4.555 % |
c |    443342 |   21229   114094 |    9340    6398  1054100   164.8 |  4.566 % |
c |    443492 |   21229   114094 |   10274    6548  1057414   161.5 |  4.566 % |
c |    443717 |   21229   114094 |   11302    6773  1077020   159.0 |  4.566 % |
c |    444054 |   21229   114094 |   12432    7110  1097269   154.3 |  4.566 % |
c |    444561 |   21229   114094 |   13675    7617  1130196   148.4 |  4.566 % |
c |    445320 |   21229   114094 |   15043    8376  1186676   141.7 |  4.566 % |
c |    446460 |   21229   114094 |   16547    9516  1280907   134.6 |  4.566 % |
c |    448168 |   21229   114094 |   18202   11224  1431052   127.5 |  4.566 % |
c |    450730 |   21229   114094 |   20022   13786  2056496   149.2 |  4.566 % |
c |    454574 |   21201   113885 |   21995   17421  2738533   157.2 |  4.710 % |
c |    460340 |   21201   113885 |   24195   23187  3378032   145.7 |  4.710 % |
c ==============================================================================
c (current CPU-time: 684.861 s)
c ==============================================================================
c [1mFound solution: 2001[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    463454 |   21498   114659 |    6449   15258  1684158   110.4 |  4.710 % |
c   -- subsuming                       
c   -- var.elim.:  857/857          
c   -- var.elim.:  228/228          
c   -- var.elim.:  128/128          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  19/19          
c |    463454 |   21223   114145 |      --   15258       --      -- |     --   | -275/-513
c |    463454 |   21223   114145 |    8489   15258  1684158   110.4 |  4.710 % |
c |    463554 |   21223   114145 |    9338    6882   494448    71.8 |  4.721 % |
c |    463704 |   21223   114145 |   10271    7032   502564    71.5 |  4.721 % |
c |    463929 |   21196   113932 |   11284    7241   510872    70.6 |  4.781 % |
c |    464266 |   21196   113932 |   12413    7578   533666    70.4 |  4.781 % |
c |    464773 |   21196   113932 |   13654    8085   576465    71.3 |  4.781 % |
c |    465532 |   21196   113932 |   15020    8844   620284    70.1 |  4.781 % |
c |    466674 |   21190   113889 |   16517    9950   740620    74.4 |  4.818 % |
c |    468384 |   21190   113889 |   18169   11660   952312    81.7 |  4.818 % |
c |    470946 |   21190   113889 |   19985   14222  1408155    99.0 |  4.818 % |
c |    474792 |   21182   113855 |   21976   18066  2205162   122.1 |  4.854 % |
c ==============================================================================
c (current CPU-time: 704.384 s)
c ==============================================================================
c [1mFound solution: 2000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    477632 |   21477   114624 |    6443   20906  2753223   131.7 |  4.854 % |
c   -- subsuming                       
c   -- var.elim.:  698/698          
c   -- var.elim.:  243/243          
c   -- var.elim.:  125/125          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |    477632 |   21205   114166 |      --   20906       --      -- |     --   | -272/-457
c |    477632 |   21205   114166 |    8482   18032  1998332   110.8 |  4.854 % |
c |    477732 |   21205   114166 |    9330    8115   936286   115.4 |  4.866 % |
c |    477885 |   21205   114166 |   10263    8268   949423   114.8 |  4.866 % |
c |    478111 |   21205   114166 |   11289    8494   954275   112.3 |  4.866 % |
c |    478448 |   21205   114166 |   12418    8831   986791   111.7 |  4.866 % |
c |    478955 |   21205   114166 |   13660    9338  1034681   110.8 |  4.866 % |
c |    479714 |   21205   114166 |   15026   10097  1098980   108.8 |  4.866 % |
c |    480853 |   21199   114121 |   16524   11235  1165004   103.7 |  4.902 % |
c |    482562 |   21199   114121 |   18176   12944  1352499   104.5 |  4.902 % |
c |    485124 |   21199   114121 |   19994   15506  1576108   101.6 |  4.902 % |
c |    488968 |   21199   114121 |   21993   19350  1967603   101.7 |  4.903 % |
c |    494736 |   21199   114121 |   24193   14716  1093565    74.3 |  4.902 % |
c |    503385 |   21199   114121 |   26612   23365  2593031   111.0 |  4.902 % |
c |    516359 |   21199   114121 |   29273   23204  2675495   115.3 |  4.902 % |
c |    535822 |   21199   114121 |   32201   27690  4608726   166.4 |  4.903 % |
c ==============================================================================
c (current CPU-time: 799.306 s)
c ==============================================================================
c [1mFound solution: 1990[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    540617 |   21497   114879 |    6449   32485  5326859   164.0 |  4.903 % |
c   -- subsuming                       
c   -- var.elim.:  513/513          
c   -- var.elim.:  198/198          
c   -- var.elim.:  126/126          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |    540617 |   21224   114362 |      --   32485       --      -- |     --   | -273/-516
c |    540617 |   21224   114362 |    8489   32485  5326859   164.0 |  4.903 % |
c |    540718 |   21224   114362 |    9338    6699   672812   100.4 |  4.913 % |
c |    540869 |   21224   114362 |   10272    6850   692109   101.0 |  4.913 % |
c |    541094 |   21224   114362 |   11299    7075   704061    99.5 |  4.913 % |
c |    541431 |   21224   114362 |   12429    7412   756282   102.0 |  4.913 % |
c |    541937 |   21224   114362 |   13672    7918   810274   102.3 |  4.913 % |
c |    542696 |   21224   114362 |   15039    8677   933210   107.5 |  4.913 % |
c |    543835 |   21224   114362 |   16543    9816  1009797   102.9 |  4.913 % |
c |    545543 |   21209   114285 |   18185   11002  1111723   101.0 |  4.997 % |
c |    548106 |   21184   114092 |   19980   13490  1353371   100.3 |  5.129 % |
c |    551950 |   21184   114092 |   21978   17334  1887563   108.9 |  5.129 % |
c ==============================================================================
c (current CPU-time: 817.685 s)
c ==============================================================================
c [1mFound solution: 1988[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    552567 |   21488   114889 |    6446   17951  1967087   109.6 |  5.129 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1056          
c   -- var.elim.:  1056/1056          
c   -- var.elim.:  231/231          
c   -- var.elim.:  126/126          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |    552567 |   21209   114355 |      --   17951       --      -- |     --   | -279/-533
c |    552567 |   21209   114355 |    8483   17950  1967084   109.6 |  5.129 % |
c |    552667 |   21209   114355 |    9331    8078   727082    90.0 |  5.140 % |
c |    552817 |   21209   114355 |   10265    8228   737410    89.6 |  5.140 % |
c |    553042 |   21209   114355 |   11291    8453   762245    90.2 |  5.140 % |
c |    553381 |   21195   114243 |   12412    8745   782213    89.4 |  5.225 % |
c |    553887 |   21195   114243 |   13653    9251   815253    88.1 |  5.225 % |
c |    554649 |   21195   114243 |   15019   10013   900531    89.9 |  5.225 % |
c |    555788 |   21195   114243 |   16521   11152  1002019    89.9 |  5.225 % |
c |    557496 |   21195   114243 |   18173   12860  1216507    94.6 |  5.225 % |
c |    560059 |   21195   114243 |   19990   15423  1527981    99.1 |  5.225 % |
c ==============================================================================
c (current CPU-time: 830.796 s)
c ==============================================================================
c [1mFound solution: 1986[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    561020 |   21497   115027 |    6449   16384  1698155   103.6 |  5.225 % |
c   -- subsuming                       
c   -- var.elim.:  662/662          
c   -- var.elim.:  225/225          
c   -- var.elim.:  126/126          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  18/18          
c |    561020 |   21219   114502 |      --   16384       --      -- |     --   | -278/-524
c |    561020 |   21219   114502 |    8487   16327  1687344   103.3 |  5.225 % |
c |    561120 |   21219   114502 |    9336    7357   664098    90.3 |  5.236 % |
c |    561271 |   21219   114502 |   10269    7508   685072    91.2 |  5.236 % |
c |    561496 |   21219   114502 |   11296    7733   694885    89.9 |  5.236 % |
c |    561833 |   21219   114502 |   12426    8070   728933    90.3 |  5.236 % |
c |    562340 |   21219   114502 |   13669    8577   751502    87.6 |  5.236 % |
c |    563101 |   21219   114502 |   15036    9338   847790    90.8 |  5.236 % |
c |    564240 |   21219   114502 |   16539   10477   994672    94.9 |  5.236 % |
c |    565948 |   21219   114502 |   18193   12185  1163390    95.5 |  5.236 % |
c |    568510 |   21219   114502 |   20013   14747  1496372   101.5 |  5.236 % |
c ==============================================================================
c (current CPU-time: 844.203 s)
c ==============================================================================
c [1mFound solution: 1985[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    570118 |   21521   115286 |    6456   16355  1655083   101.2 |  5.236 % |
c   -- subsuming                       
c   -- var.elim.:  377/377          
c   -- var.elim.:  218/218          
c   -- var.elim.:  126/126          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |    570118 |   21245   114763 |      --   16355       --      -- |     --   | -276/-522
c |    570118 |   21245   114763 |    8498   16355  1655083   101.2 |  5.236 % |
c |    570220 |   21245   114763 |    9347    7372   606392    82.3 |  5.246 % |
c |    570370 |   21245   114763 |   10282    7522   620086    82.4 |  5.246 % |
c |    570595 |   21237   114715 |   11306    7745   625717    80.8 |  5.294 % |
c |    570933 |   21231   114671 |   12433    8082   652431    80.7 |  5.330 % |
c |    571439 |   21231   114671 |   13677    8588   704927    82.1 |  5.330 % |
c |    572199 |   21231   114671 |   15044    9348   814758    87.2 |  5.330 % |
c |    573338 |   21225   114624 |   16544   10308   925261    89.8 |  5.366 % |
c |    575046 |   21225   114624 |   18199   12016  1091336    90.8 |  5.366 % |
c |    577608 |   21225   114624 |   20018   14578  1381783    94.8 |  5.366 % |
c |    581453 |   21225   114624 |   22020   18423  1839896    99.9 |  5.366 % |
c ==============================================================================
c (current CPU-time: 862.721 s)
c ==============================================================================
c [1mFound solution: 1984[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    581985 |   21527   115408 |    6458   18955  1899935   100.2 |  5.366 % |
c   -- subsuming                       
c   -- var.elim.:  649/649          
c   -- var.elim.:  229/229          
c   -- var.elim.:  126/126          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |    581985 |   21250   114886 |      --   18955       --      -- |     --   | -277/-521
c |    581985 |   21250   114886 |    8500   18949  1899903   100.3 |  5.366 % |
c |    582085 |   21250   114886 |    9350    8522   725533    85.1 |  5.378 % |
c |    582235 |   21250   114886 |   10285    8672   739952    85.3 |  5.378 % |
c |    582461 |   21250   114886 |   11313    8898   760932    85.5 |  5.378 % |
c |    582800 |   21250   114886 |   12444    9237   789955    85.5 |  5.378 % |
c |    583306 |   21250   114886 |   13689    9743   858580    88.1 |  5.378 % |
c |    5#### 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.72 0.91 0.90 2/54 11338
Raw data (stat): 11338 (runsolver) R 11337 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481948332 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.0002 s]
Raw data (loadavg): 0.76 0.91 0.90 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 9254 0 0 0 962 35 0 0 25 0 1 0 481948332 18128896 3437 4294967295 134512640 134672761 3221224544 3221222924 1075325888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4426 3437 603 41 0 4385 0
vsize: 17704
[startup+19.9999 s]
Raw data (loadavg): 0.80 0.91 0.90 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 15530 0 0 0 1933 65 0 0 25 0 1 0 481948332 16527360 3319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4035 3319 603 41 0 3994 0
vsize: 16140
[startup+30.0015 s]
Raw data (loadavg): 0.83 0.92 0.90 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 16854 0 0 0 2927 70 0 0 25 0 1 0 481948332 19644416 3991 4294967295 134512640 134672761 3221224544 3221223552 134522547 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4796 3991 603 41 0 4755 0
vsize: 19184
[startup+40.0015 s]
Raw data (loadavg): 0.85 0.92 0.90 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 19647 0 0 0 3914 81 0 0 25 0 1 0 481948332 20930560 4295 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5110 4295 603 41 0 5069 0
vsize: 20440
[startup+50.0022 s]
Raw data (loadavg): 0.88 0.92 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 22876 0 0 0 4900 96 0 0 25 0 1 0 481948332 20762624 4218 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4218 603 41 0 5028 0
vsize: 20276
[startup+60.0024 s]
Raw data (loadavg): 0.89 0.92 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 23373 0 0 0 5897 99 0 0 25 0 1 0 481948332 21151744 4351 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5164 4351 603 41 0 5123 0
vsize: 20656
[startup+70.0032 s]
Raw data (loadavg): 0.91 0.92 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 24396 0 0 0 6894 102 0 0 25 0 1 0 481948332 25235456 5374 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6161 5374 603 41 0 6120 0
vsize: 24644
[startup+80.0033 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 24479 0 0 0 7894 102 0 0 25 0 1 0 481948332 25698304 5457 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6274 5457 603 41 0 6233 0
vsize: 25096
[startup+90.0037 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 25084 0 0 0 8893 103 0 0 25 0 1 0 481948332 28082176 6062 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6856 6062 603 41 0 6815 0
vsize: 27424
[startup+100.004 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 25259 0 0 0 9893 103 0 0 25 0 1 0 481948332 28737536 6237 4294967295 134512640 134672761 3221224544 3221223668 134566007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7016 6237 603 41 0 6975 0
vsize: 28064
[startup+110.005 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 25845 0 0 0 10889 107 0 0 25 0 1 0 481948332 29081600 6326 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7100 6326 603 41 0 7059 0
vsize: 28400
[startup+120.005 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 25845 0 0 0 11889 107 0 0 25 0 1 0 481948332 29081600 6326 4294967295 134512640 134672761 3221224544 3221223584 134614340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7100 6326 603 41 0 7059 0
vsize: 28400
[startup+130.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 25845 0 0 0 12890 107 0 0 25 0 1 0 481948332 29081600 6326 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7100 6326 603 41 0 7059 0
vsize: 28400
[startup+140.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 26394 0 0 0 13888 108 0 0 25 0 1 0 481948332 31444992 6875 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7677 6875 603 41 0 7636 0
vsize: 30708
[startup+150.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 26697 0 0 0 14888 109 0 0 25 0 1 0 481948332 32583680 7178 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7955 7178 603 41 0 7914 0
vsize: 31820
[startup+160.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 26697 0 0 0 15888 109 0 0 25 0 1 0 481948332 32583680 7178 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7955 7178 603 41 0 7914 0
vsize: 31820
[startup+170.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 27247 0 0 0 16887 110 0 0 25 0 1 0 481948332 34820096 7728 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8501 7728 603 41 0 8460 0
vsize: 34004
[startup+180.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 28497 0 0 0 17884 112 0 0 25 0 1 0 481948332 39915520 8943 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9745 8943 603 41 0 9704 0
vsize: 38980
[startup+190.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 28497 0 0 0 18885 112 0 0 25 0 1 0 481948332 39915520 8943 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9745 8943 603 41 0 9704 0
vsize: 38980
[startup+200.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 28818 0 0 0 19884 114 0 0 25 0 1 0 481948332 41238528 9264 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9264 603 41 0 10027 0
vsize: 40272
[startup+210.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 30682 0 0 0 20880 118 0 0 25 0 1 0 481948332 48947200 11128 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11950 11128 603 41 0 11909 0
vsize: 47800
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 32250 0 0 0 21877 121 0 0 25 0 1 0 481948332 55377920 12696 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12696 603 41 0 13479 0
vsize: 54080
[startup+230.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 32599 0 0 0 22876 122 0 0 25 0 1 0 481948332 56565760 13009 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13810 13009 603 41 0 13769 0
vsize: 55240
[startup+240.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33187 0 0 0 23874 124 0 0 25 0 1 0 481948332 56553472 13008 4294967295 134512640 134672761 3221224544 3221223728 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13807 13008 603 41 0 13766 0
vsize: 55228
[startup+250.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33187 0 0 0 24873 124 0 0 25 0 1 0 481948332 56553472 13008 4294967295 134512640 134672761 3221224544 3221223688 134616258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13807 13008 603 41 0 13766 0
vsize: 55228
[startup+260.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33481 0 0 0 25871 126 0 0 25 0 1 0 481948332 56516608 12999 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13798 12999 603 41 0 13757 0
vsize: 55192
[startup+270.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33481 0 0 0 26871 127 0 0 25 0 1 0 481948332 56516608 12999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13798 12999 603 41 0 13757 0
vsize: 55192
[startup+280.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33481 0 0 0 27870 127 0 0 25 0 1 0 481948332 56516608 12999 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13798 12999 603 41 0 13757 0
vsize: 55192
[startup+290.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33481 0 0 0 28871 127 0 0 25 0 1 0 481948332 56516608 12999 4294967295 134512640 134672761 3221224544 3221223584 134612885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13798 12999 603 41 0 13757 0
vsize: 55192
[startup+300.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33733 0 0 0 29869 129 0 0 25 0 1 0 481948332 56516608 12999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13798 12999 603 41 0 13757 0
vsize: 55192
[startup+310.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33733 0 0 0 30869 129 0 0 25 0 1 0 481948332 56516608 12999 4294967295 134512640 134672761 3221224544 3221223728 134615614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13798 12999 603 41 0 13757 0
vsize: 55192
[startup+320.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33989 0 0 0 31868 130 0 0 25 0 1 0 481948332 56442880 12985 4294967295 134512640 134672761 3221224544 3221223628 1074733103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12985 603 41 0 13739 0
vsize: 55120
[startup+330.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33989 0 0 0 32869 130 0 0 25 0 1 0 481948332 56442880 12985 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12985 603 41 0 13739 0
vsize: 55120
[startup+340.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33989 0 0 0 33870 130 0 0 25 0 1 0 481948332 56442880 12985 4294967295 134512640 134672761 3221224544 3221223744 134610683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 12985 603 41 0 13739 0
vsize: 55120
[startup+350.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 33989 0 0 0 34869 130 0 0 25 0 1 0 481948332 56442880 12985 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12985 603 41 0 13739 0
vsize: 55120
[startup+360.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34247 0 0 0 35867 132 0 0 25 0 1 0 481948332 56442880 12989 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12989 603 41 0 13739 0
vsize: 55120
[startup+370.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 36865 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+380.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 37865 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+390.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 38865 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+400.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 39865 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+410.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 40866 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+420.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 41866 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+430.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 42867 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+440.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 43867 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+450.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34509 0 0 0 44867 134 0 0 25 0 1 0 481948332 56442880 12993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12993 603 41 0 13739 0
vsize: 55120
[startup+460.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34773 0 0 0 45866 135 0 0 25 0 1 0 481948332 56442880 12997 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 12997 603 41 0 13739 0
vsize: 55120
[startup+470.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34773 0 0 0 46865 135 0 0 25 0 1 0 481948332 56442880 12997 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12997 603 41 0 13739 0
vsize: 55120
[startup+480.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34773 0 0 0 47865 135 0 0 25 0 1 0 481948332 56442880 12997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12997 603 41 0 13739 0
vsize: 55120
[startup+490.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34773 0 0 0 48865 136 0 0 25 0 1 0 481948332 56442880 12997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 12997 603 41 0 13739 0
vsize: 55120
[startup+500.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34773 0 0 0 49865 136 0 0 25 0 1 0 481948332 56442880 12997 4294967295 134512640 134672761 3221224544 3221223696 134616479 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12997 603 41 0 13739 0
vsize: 55120
[startup+510.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 34773 0 0 0 50867 136 0 0 25 0 1 0 481948332 56442880 12997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 12997 603 41 0 13739 0
vsize: 55120
[startup+520.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35041 0 0 0 51864 138 0 0 25 0 1 0 481948332 56442880 13003 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13003 603 41 0 13739 0
vsize: 55120
[startup+530.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35041 0 0 0 52864 138 0 0 25 0 1 0 481948332 56442880 13003 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13003 603 41 0 13739 0
vsize: 55120
[startup+540.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35041 0 0 0 53865 138 0 0 25 0 1 0 481948332 56442880 13003 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13003 603 41 0 13739 0
vsize: 55120
[startup+550.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35041 0 0 0 54865 138 0 0 25 0 1 0 481948332 56442880 13003 4294967295 134512640 134672761 3221224544 3221223728 134615998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13003 603 41 0 13739 0
vsize: 55120
[startup+560.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35041 0 0 0 55865 138 0 0 25 0 1 0 481948332 56442880 13003 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13003 603 41 0 13739 0
vsize: 55120
[startup+570.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35041 0 0 0 56865 138 0 0 25 0 1 0 481948332 56442880 13003 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13003 603 41 0 13739 0
vsize: 55120
[startup+580.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35309 0 0 0 57863 140 0 0 25 0 1 0 481948332 56442880 13005 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 13005 603 41 0 13739 0
vsize: 55120
[startup+590.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35309 0 0 0 58863 140 0 0 25 0 1 0 481948332 56442880 13005 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13005 603 41 0 13739 0
vsize: 55120
[startup+600.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11338
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35583 0 0 0 59861 142 0 0 25 0 1 0 481948332 56442880 13011 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 13011 603 41 0 13739 0
vsize: 55120
[startup+610.084 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 11378
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35583 0 0 0 60859 142 0 0 25 0 1 0 481948332 56442880 13011 4294967295 134512640 134672761 3221224544 3221223728 134615994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13011 603 41 0 13739 0
vsize: 55120
[startup+620.085 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 11391
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35859 0 0 0 61857 143 0 0 25 0 1 0 481948332 56442880 13015 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13015 603 41 0 13739 0
vsize: 55120
[startup+630.086 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 11391
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35859 0 0 0 62857 143 0 0 25 0 1 0 481948332 56442880 13015 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13015 603 41 0 13739 0
vsize: 55120
[startup+640.085 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 11391
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35859 0 0 0 63858 143 0 0 25 0 1 0 481948332 56442880 13015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13015 603 41 0 13739 0
vsize: 55120
[startup+650.085 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 11391
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 35859 0 0 0 64858 143 0 0 25 0 1 0 481948332 56442880 13015 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13015 603 41 0 13739 0
vsize: 55120
[startup+660.085 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 11391
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36135 0 0 0 65856 145 0 0 25 0 1 0 481948332 56442880 13017 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13017 603 41 0 13739 0
vsize: 55120
[startup+670.085 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 11391
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36135 0 0 0 66856 145 0 0 25 0 1 0 481948332 56442880 13017 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13017 603 41 0 13739 0
vsize: 55120
[startup+680.085 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36135 0 0 0 67856 145 0 0 25 0 1 0 481948332 56442880 13017 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13017 603 41 0 13739 0
vsize: 55120
[startup+690.086 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36417 0 0 0 68855 147 0 0 25 0 1 0 481948332 56442880 13023 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13023 603 41 0 13739 0
vsize: 55120
[startup+700.085 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36417 0 0 0 69855 147 0 0 25 0 1 0 481948332 56442880 13023 4294967295 134512640 134672761 3221224544 3221223648 134603769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13023 603 41 0 13739 0
vsize: 55120
[startup+710.085 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36699 0 0 0 70853 149 0 0 25 0 1 0 481948332 56442880 13025 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13025 603 41 0 13739 0
vsize: 55120
[startup+720.085 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36699 0 0 0 71853 149 0 0 25 0 1 0 481948332 56442880 13025 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13025 603 41 0 13739 0
vsize: 55120
[startup+730.086 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36699 0 0 0 72854 149 0 0 25 0 1 0 481948332 56442880 13025 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13025 603 41 0 13739 0
vsize: 55120
[startup+740.085 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36699 0 0 0 73854 149 0 0 25 0 1 0 481948332 56442880 13025 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13025 603 41 0 13739 0
vsize: 55120
[startup+750.086 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36700 0 0 0 74853 149 0 0 25 0 1 0 481948332 56442880 13026 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 13026 603 41 0 13739 0
vsize: 55120
[startup+760.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36700 0 0 0 75853 149 0 0 25 0 1 0 481948332 56442880 13026 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13026 603 41 0 13739 0
vsize: 55120
[startup+770.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36700 0 0 0 76853 149 0 0 25 0 1 0 481948332 56442880 13026 4294967295 134512640 134672761 3221224544 3221223508 1075347030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13026 603 41 0 13739 0
vsize: 55120
[startup+780.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36700 0 0 0 77854 149 0 0 25 0 1 0 481948332 56442880 13026 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13026 603 41 0 13739 0
vsize: 55120
[startup+790.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36700 0 0 0 78854 149 0 0 25 0 1 0 481948332 56442880 13026 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13026 603 41 0 13739 0
vsize: 55120
[startup+800.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36700 0 0 0 79854 149 0 0 25 0 1 0 481948332 56442880 13026 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13026 603 41 0 13739 0
vsize: 55120
[startup+810.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 36990 0 0 0 80852 150 0 0 25 0 1 0 481948332 56442880 13034 4294967295 134512640 134672761 3221224544 3221223728 134615557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13034 603 41 0 13739 0
vsize: 55120
[startup+820.086 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 37278 0 0 0 81851 151 0 0 25 0 1 0 481948332 56442880 13036 4294967295 134512640 134672761 3221224544 3221223640 134616320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13036 603 41 0 13739 0
vsize: 55120
[startup+830.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 37278 0 0 0 82851 151 0 0 25 0 1 0 481948332 56442880 13036 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13036 603 41 0 13739 0
vsize: 55120
[startup+840.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 37570 0 0 0 83849 153 0 0 25 0 1 0 481948332 56442880 13040 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13040 603 41 0 13739 0
vsize: 55120
[startup+850.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 37864 0 0 0 84847 155 0 0 25 0 1 0 481948332 56442880 13044 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13044 603 41 0 13739 0
vsize: 55120
[startup+860.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 37864 0 0 0 85847 155 0 0 25 0 1 0 481948332 56442880 13044 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13044 603 41 0 13739 0
vsize: 55120
[startup+870.088 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 86844 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+880.088 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 87844 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+890.088 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 88844 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+900.088 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 89843 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+910.088 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 90844 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+920.088 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 91844 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+930.089 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 92844 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+940.089 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11393
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 93844 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+950.089 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 94844 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+960.089 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 95845 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+970.089 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 96845 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+980.089 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 97845 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+990.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 98845 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+1000.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38162 0 0 0 99845 158 0 0 25 0 1 0 481948332 56442880 13048 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13048 603 41 0 13739 0
vsize: 55120
[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38163 0 0 0 100845 158 0 0 25 0 1 0 481948332 56442880 13049 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13049 603 41 0 13739 0
vsize: 55120
[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38163 0 0 0 101846 158 0 0 25 0 1 0 481948332 56442880 13049 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13049 603 41 0 13739 0
vsize: 55120
[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38163 0 0 0 102846 158 0 0 25 0 1 0 481948332 56442880 13049 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13049 603 41 0 13739 0
vsize: 55120
[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38163 0 0 0 103846 158 0 0 25 0 1 0 481948332 56442880 13049 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13049 603 41 0 13739 0
vsize: 55120
[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38163 0 0 0 104846 158 0 0 25 0 1 0 481948332 56442880 13049 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13049 603 41 0 13739 0
vsize: 55120
[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38163 0 0 0 105846 158 0 0 25 0 1 0 481948332 56442880 13049 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13049 603 41 0 13739 0
vsize: 55120
[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38163 0 0 0 106846 158 0 0 25 0 1 0 481948332 56442880 13049 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 13049 603 41 0 13739 0
vsize: 55120
[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38164 0 0 0 107846 158 0 0 25 0 1 0 481948332 56442880 13050 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13050 603 41 0 13739 0
vsize: 55120
[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 38166 0 0 0 108846 158 0 0 25 0 1 0 481948332 56442880 13052 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13780 13052 603 41 0 13739 0
vsize: 55120
[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 39693 0 0 0 109841 163 0 0 25 0 1 0 481948332 62758912 14579 4294967295 134512640 134672761 3221224544 3221223600 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15322 14579 603 41 0 15281 0
vsize: 61288
[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 39693 0 0 0 110842 163 0 0 25 0 1 0 481948332 62627840 14566 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15290 14566 603 41 0 15249 0
vsize: 61160
[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 39693 0 0 0 111842 163 0 0 25 0 1 0 481948332 62627840 14566 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15290 14566 603 41 0 15249 0
vsize: 61160
[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 39693 0 0 0 112842 163 0 0 25 0 1 0 481948332 62627840 14566 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15290 14566 603 41 0 15249 0
vsize: 61160
[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 39693 0 0 0 113842 163 0 0 25 0 1 0 481948332 62627840 14566 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15290 14566 603 41 0 15249 0
vsize: 61160
[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 40542 0 0 0 114840 165 0 0 25 0 1 0 481948332 66056192 15403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16127 15403 603 41 0 16086 0
vsize: 64508
[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 40542 0 0 0 115840 165 0 0 25 0 1 0 481948332 66056192 15403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16127 15403 603 41 0 16086 0
vsize: 64508
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 40542 0 0 0 116841 165 0 0 25 0 1 0 481948332 66056192 15403 4294967295 134512640 134672761 3221224544 3221223584 134612504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16127 15403 603 41 0 16086 0
vsize: 64508
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 40542 0 0 0 117841 165 0 0 25 0 1 0 481948332 66056192 15403 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16127 15403 603 41 0 16086 0
vsize: 64508
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 41001 0 0 0 118840 165 0 0 25 0 1 0 481948332 67993600 15862 4294967295 134512640 134672761 3221224544 3221223584 134612653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16600 15862 603 41 0 16559 0
vsize: 66400
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 11395
Raw data (stat): 11338 (minisat+) R 11337 24215 24214 0 -1 0 41975 0 0 0 119838 167 0 0 25 0 1 0 481948332 72024064 16836 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17584 16836 603 41 0 17543 0
vsize: 70336
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 11395
Raw data (stat): 11338 (minisat+) Z 11337 24215 24214 0 -1 12 41976 0 0 0 119838 171 0 0 25 0 1 0 481948332 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.13
CPU time (s): 1200.11
CPU user time (s): 1198.39
CPU system time (s): 1.71774
CPU usage (%): 99.9982
Max. virtual memory (Kb): 70336
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####