PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos5.opb
MD5SUM	e6bff154156b54af3a9a38f7579209b6
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	17324
Optimality of the best value was proved	NO
Number of terms in the objective function	163
Biggest coefficient in the objective function	1024
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	74742
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	8192
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	74742
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06984
Number of variables	163
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	102
Trace number 20560

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 21:21:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14714 boxname=wulflinc25 idbench=1132 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e6bff154156b54af3a9a38f7579209b6  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos5.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos5.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos5.opb
IDLAUNCH: 14714
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        788960 kB
Buffers:          3008 kB
Cached:         222036 kB
SwapCached:        716 kB
Active:          39912 kB
Inactive:       187076 kB
HighTotal:      131008 kB
HighFree:         7924 kB
LowTotal:       903652 kB
LowFree:        781036 kB
SwapTotal:     2097892 kB
SwapFree:      2096236 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12952 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 21:41:57 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 14714 7 1200.34 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:   10
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   10
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   10
c ---[  62]---> Sorter-cost:  382     Base:
c ---[  61]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost: 1471     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost: 1060     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost: 1241     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1058     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1269     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  216     Base:
c ---[  50]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  548     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  351     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1195     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  345     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost: 1020     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1259     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  319     Base: 2 2 2 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 2 2 2
c ---[   0]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   28565    68464 |    8569       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18763          
c   -- var.elim.:  2000/18763          
c   -- var.elim.:  3000/18763          
c   -- var.elim.:  4000/18763          
c   -- var.elim.:  5000/18763          
c   -- var.elim.:  6000/18763          
c   -- var.elim.:  7000/18763          
c   -- var.elim.:  8000/18763          
c   -- var.elim.:  9000/18763          
c   -- var.elim.:  10000/18763          
c   -- var.elim.:  11000/18763          
c   -- var.elim.:  12000/18763          
c   -- var.elim.:  13000/18763          
c   -- var.elim.:  14000/18763          
c   -- var.elim.:  15000/18763          
c   -- var.elim.:  16000/18763          
c   -- var.elim.:  17000/18763          
c   -- var.elim.:  18000/18763          
c   -- var.elim.:  18763/18763          
c   -- var.elim.:  1000/8798          
c   -- var.elim.:  2000/8798          
c   -- var.elim.:  3000/8798          
c   -- var.elim.:  4000/8798          
c   -- var.elim.:  5000/8798          
c   -- var.elim.:  6000/8798          
c   -- var.elim.:  7000/8798          
c   -- var.elim.:  8000/8798          
c   -- var.elim.:  8798/8798          
c   -- var.elim.:  1000/1443          
c   -- var.elim.:  1443/1443          
c   -- var.elim.:  672/672          
c   -- subsuming                       
c   -- var.elim.:  1000/7898          
c   -- var.elim.:  2000/7898          
c   -- var.elim.:  3000/7898          
c   -- var.elim.:  4000/7898          
c   -- var.elim.:  5000/7898          
c   -- var.elim.:  6000/7898          
c   -- var.elim.:  7000/7898          
c   -- var.elim.:  7898/7898          
c   -- var.elim.:  1000/4083          
c   -- var.elim.:  2000/4083          
c   -- var.elim.:  3000/4083          
c   -- var.elim.:  4000/4083          
c   -- var.elim.:  4083/4083          
c   -- subsuming                       
c   -- var.elim.:  1000/1830          
c   -- var.elim.:  1830/1830          
c   -- var.elim.:  546/546          
c   -- subsuming                       
c   -- var.elim.:  426/426          
c |         0 |   18638    93433 |      --       0       --      -- |     --   | -9924/25050
c |         0 |   18638    93433 |    7455       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.82427 s)
c ==============================================================================
c [1mFound solution: 63104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2665     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         2 |   25127   108674 |    7538       2       35    17.5 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2893          
c   -- var.elim.:  2000/2893          
c   -- var.elim.:  2893/2893          
c   -- var.elim.:  1000/1612          
c   -- var.elim.:  1612/1612          
c   -- subsuming                       
c   -- var.elim.:  420/420          
c   -- var.elim.:  310/310          
c   -- subsuming                       
c   -- var.elim.:  138/138          
c |         2 |   24185   111924 |      --       2       --      -- |     --   | -942/3251
c |         2 |   24185   111924 |    9674       2       35    17.5 |  0.000 % |
c ==============================================================================
c (current CPU-time: 5.69713 s)
c ==============================================================================
c [1mFound solution: 35326[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        56 |   24846   113763 |    7453      56      235     4.2 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1045          
c   -- var.elim.:  1045/1045          
c   -- var.elim.:  564/564          
c   -- subsuming                       
c   -- var.elim.:  322/322          
c |        56 |   24389   113444 |      --      56       --      -- |     --   | -457/-318
c |        56 |   24389   113444 |    9755      56      235     4.2 |  0.000 % |
c ==============================================================================
c (current CPU-time: 6.22705 s)
c ==============================================================================
c [1mFound solution: 31462[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       129 |   24833   114751 |    7449     129     1031     8.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  818/818          
c   -- var.elim.:  450/450          
c   -- var.elim.:  23/23          
c |       129 |   24474   114653 |      --     129       --      -- |     --   | -359/-97
c |       129 |   24474   114653 |    9789     129     1031     8.0 |  0.000 % |
c |       229 |   24474   114653 |   10768     229     2171     9.5 |  0.837 % |
c ==============================================================================
c (current CPU-time: 6.74198 s)
c ==============================================================================
c [1mFound solution: 20544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       254 |   24882   115814 |    7464     254     2271     8.9 |  0.837 % |
c   -- subsuming                       
c   -- var.elim.:  770/770          
c   -- var.elim.:  387/387          
c |       254 |   24567   115512 |      --     254       --      -- |     --   | -315/-301
c |       254 |   24567   115512 |    9826     254     2271     8.9 |  0.837 % |
c |       354 |   24567   115512 |   10809     354     3367     9.5 |  0.877 % |
c ==============================================================================
c (current CPU-time: 7.30289 s)
c ==============================================================================
c [1mFound solution: 20543[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       424 |   24631   115719 |    7389     424     4316    10.2 |  0.877 % |
c   -- subsuming                       
c   -- var.elim.:  350/350          
c   -- var.elim.:  101/101          
c |       424 |   24600   115881 |      --     424       --      -- |     --   | -31/163
c |       424 |   24600   115881 |    9840     424     4316    10.2 |  0.877 % |
c |       524 |   24600   115881 |   10824     524     6165    11.8 |  0.887 % |
c ==============================================================================
c (current CPU-time: 7.82781 s)
c ==============================================================================
c [1mFound solution: 20523[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       666 |   24669   116107 |    7400     666     7125    10.7 |  0.887 % |
c   -- subsuming                       
c   -- var.elim.:  154/154          
c   -- var.elim.:  113/113          
c |       666 |   24634   116278 |      --     666       --      -- |     --   | -35/172
c |       666 |   24634   116278 |    9853     666     7125    10.7 |  0.887 % |
c |       766 |   24634   116278 |   10838     766     7654    10.0 |  0.897 % |
c ==============================================================================
c (current CPU-time: 8.29474 s)
c ==============================================================================
c [1mFound solution: 17655[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       851 |   24885   116918 |    7465     849    12731    15.0 |  0.897 % |
c   -- subsuming                       
c   -- var.elim.:  488/488          
c   -- var.elim.:  233/233          
c |       851 |   24686   116724 |      --     849       --      -- |     --   | -199/-193
c |       851 |   24686   116724 |    9874     849    12731    15.0 |  0.897 % |
c |       951 |   24686   116724 |   10861     949    16234    17.1 |  0.948 % |
c |      1104 |   24678   116660 |   11944    1091    18997    17.4 |  0.979 % |
c |      1329 |   24678   116660 |   13138    1316    22814    17.3 |  0.979 % |
c ==============================================================================
c (current CPU-time: 9.15261 s)
c ==============================================================================
c [1mFound solution: 17450[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1406 |   24755   116917 |    7426    1393    26630    19.1 |  0.979 % |
c   -- subsuming                       
c   -- var.elim.:  414/414          
c   -- var.elim.:  130/130          
c |      1406 |   24715   117058 |      --    1393       --      -- |     --   | -40/142
c |      1406 |   24715   117058 |    9886    1393    26630    19.1 |  0.979 % |
c |      1506 |   24715   117058 |   10874    1493    28731    19.2 |  1.010 % |
c ==============================================================================
c (current CPU-time: 9.70952 s)
c ==============================================================================
c [1mFound solution: 17449[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1573 |   24790   117306 |    7436    1560    32204    20.6 |  1.010 % |
c   -- subsuming                       
c   -- var.elim.:  169/169          
c   -- var.elim.:  125/125          
c |      1573 |   24752   117473 |      --    1560       --      -- |     --   | -38/168
c |      1573 |   24752   117473 |    9900    1560    32204    20.6 |  1.010 % |
c |      1673 |   24752   117473 |   10890    1660    34452    20.8 |  1.020 % |
c ==============================================================================
c (current CPU-time: 10.2614 s)
c ==============================================================================
c [1mFound solution: 17446[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1778 |   24806   117642 |    7441    1765    39237    22.2 |  1.020 % |
c   -- subsuming                       
c   -- var.elim.:  111/111          
c   -- var.elim.:  80/80          
c |      1778 |   24781   117771 |      --    1765       --      -- |     --   | -25/130
c |      1778 |   24781   117771 |    9912    1765    39237    22.2 |  1.020 % |
c ==============================================================================
c (current CPU-time: 10.6924 s)
c ==============================================================================
c [1mFound solution: 17444[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1861 |   24859   118030 |    7457    1848    41331    22.4 |  1.020 % |
c   -- subsuming                       
c   -- var.elim.:  177/177          
c   -- var.elim.:  130/130          
c |      1861 |   24820   118327 |      --    1848       --      -- |     --   | -39/298
c |      1861 |   24820   118327 |    9928    1848    41331    22.4 |  1.020 % |
c |      1961 |   24820   118327 |   10920    1948    44318    22.8 |  1.040 % |
c ==============================================================================
c (current CPU-time: 11.2443 s)
c ==============================================================================
c [1mFound solution: 17439[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2057 |   24882   118493 |    7464    2024    46765    23.1 |  1.040 % |
c   -- subsuming                       
c   -- var.elim.:  279/279          
c   -- var.elim.:  105/105          
c |      2057 |   24847   118668 |      --    2024       --      -- |     --   | -35/176
c |      2057 |   24847   118668 |    9938    2024    46765    23.1 |  1.040 % |
c |      2157 |   24847   118668 |   10932    2124    54196    25.5 |  1.082 % |
c ==============================================================================
c (current CPU-time: 11.8192 s)
c ==============================================================================
c [1mFound solution: 17438[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2213 |   24925   118927 |    7477    2180    56033    25.7 |  1.082 % |
c   -- subsuming                       
c   -- var.elim.:  177/177          
c   -- var.elim.:  129/129          
c |      2213 |   24883   119160 |      --    2180       --      -- |     --   | -42/234
c |      2213 |   24883   119160 |    9953    2180    56033    25.7 |  1.082 % |
c |      2314 |   24883   119160 |   10948    2281    58904    25.8 |  1.092 % |
c |      2467 |   24883   119160 |   12043    2434    63883    26.2 |  1.092 % |
c ==============================================================================
c (current CPU-time: 12.7111 s)
c ==============================================================================
c [1mFound solution: 17430[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2583 |   24960   119418 |    7487    2550    67995    26.7 |  1.092 % |
c   -- subsuming                       
c   -- var.elim.:  177/177          
c   -- var.elim.:  129/129          
c |      2583 |   24920   119597 |      --    2550       --      -- |     --   | -40/180
c |      2583 |   24920   119597 |    9968    2550    67995    26.7 |  1.092 % |
c ==============================================================================
c (current CPU-time: 13.095 s)
c ==============================================================================
c [1mFound solution: 17428[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2617 |   24983   119811 |    7494    2584    69170    26.8 |  1.092 % |
c   -- subsuming                       
c   -- var.elim.:  147/147          
c   -- var.elim.:  110/110          
c |      2617 |   24952   119984 |      --    2584       --      -- |     --   | -31/174
c |      2617 |   24952   119984 |    9980    2584    69170    26.8 |  1.092 % |
c ==============================================================================
c (current CPU-time: 13.463 s)
c ==============================================================================
c [1mFound solution: 17427[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2668 |   25014   120195 |    7504    2635    69532    26.4 |  1.092 % |
c   -- subsuming                       
c   -- var.elim.:  145/145          
c   -- var.elim.:  109/109          
c |      2668 |   24984   120368 |      --    2635       --      -- |     --   | -30/174
c |      2668 |   24984   120368 |    9993    2635    69532    26.4 |  1.092 % |
c |      2770 |   24984   120368 |   10992    2737    73217    26.8 |  1.122 % |
c |      2920 |   24980   120328 |   12090    2884    78824    27.3 |  1.143 % |
c |      3146 |   24980   120328 |   13299    3110    88206    28.4 |  1.143 % |
c ==============================================================================
c (current CPU-time: 14.6398 s)
c ==============================================================================
c [1mFound solution: 17426[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3303 |   25047   120560 |    7514    3267    93765    28.7 |  1.143 % |
c   -- subsuming                       
c   -- var.elim.:  201/201          
c   -- var.elim.:  122/122          
c |      3303 |   25014   120710 |      --    3267       --      -- |     --   | -33/151
c |      3303 |   25014   120710 |   10005    3267    93765    28.7 |  1.143 % |
c ==============================================================================
c (current CPU-time: 15.0477 s)
c ==============================================================================
c [1mFound solution: 17424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3362 |   25076   120912 |    7522    3326    95642    28.8 |  1.143 % |
c   -- subsuming                       
c   -- var.elim.:  136/136          
c   -- var.elim.:  100/100          
c |      3362 |   25046   121068 |      --    3326       --      -- |     --   | -30/157
c |      3362 |   25046   121068 |   10018    3326    95642    28.8 |  1.143 % |
c ==============================================================================
c (current CPU-time: 15.4017 s)
c ==============================================================================
c [1mFound solution: 17423[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3392 |   25107   121267 |    7532    3356    97093    28.9 |  1.143 % |
c   -- subsuming                       
c   -- var.elim.:  134/134          
c   -- var.elim.:  99/99          
c |      3392 |   25078   121423 |      --    3356       --      -- |     --   | -29/157
c |      3392 |   25078   121423 |   10031    3356    97093    28.9 |  1.143 % |
c |      3492 |   25078   121423 |   11034    3456    99242    28.7 |  1.173 % |
c ==============================================================================
c (current CPU-time: 15.8476 s)
c ==============================================================================
c [1mFound solution: 17422[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3507 |   25146   121657 |    7543    3471    99735    28.7 |  1.173 % |
c   -- subsuming                       
c   -- var.elim.:  162/162          
c   -- var.elim.:  122/122          
c |      3507 |   25112   121787 |      --    3471       --      -- |     --   | -34/131
c |      3507 |   25112   121787 |   10044    3471    99735    28.7 |  1.173 % |
c |      3608 |   25112   121787 |   11049    3572   102478    28.7 |  1.183 % |
c |      3759 |   25112   121787 |   12154    3723   108518    29.1 |  1.183 % |
c |      3984 |   25112   121787 |   13369    3948   123023    31.2 |  1.183 % |
c |      4322 |   25112   121787 |   14706    4286   134184    31.3 |  1.183 % |
c ==============================================================================
c (current CPU-time: 17.2544 s)
c ==============================================================================
c [1mFound solution: 17421[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4491 |   25178   122012 |    7553    4455   138566    31.1 |  1.183 % |
c   -- subsuming                       
c   -- var.elim.:  155/155          
c   -- var.elim.:  117/117          
c |      4491 |   25146   122146 |      --    4455       --      -- |     --   | -32/135
c |      4491 |   25146   122146 |   10058    4455   138566    31.1 |  1.183 % |
c ==============================================================================
c (current CPU-time: 17.6283 s)
c ==============================================================================
c [1mFound solution: 17420[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4515 |   25211   122362 |    7563    4479   140487    31.4 |  1.183 % |
c   -- subsuming                       
c   -- var.elim.:  147/147          
c   -- var.elim.:  110/110          
c |      4515 |   25180   122498 |      --    4479       --      -- |     --   | -31/137
c |      4515 |   25180   122498 |   10072    4479   140487    31.4 |  1.183 % |
c |      4616 |   25170   122360 |   11074    4574   143196    31.3 |  1.234 % |
c |      4766 |   25170   122360 |   12182    4724   145572    30.8 |  1.234 % |
c |      4992 |   25170   122360 |   13400    4950   154173    31.1 |  1.234 % |
c ==============================================================================
c (current CPU-time: 18.6032 s)
c ==============================================================================
c [1mFound solution: 17419[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5093 |   25230   122548 |    7568    5051   162944    32.3 |  1.234 % |
c   -- subsuming                       
c   -- var.elim.:  230/230          
c   -- var.elim.:  90/90          
c |      5093 |   25202   122689 |      --    5051       --      -- |     --   | -28/142
c |      5093 |   25202   122689 |   10080    5051   162944    32.3 |  1.234 % |
c |      5194 |   25202   122689 |   11088    5152   167600    32.5 |  1.244 % |
c |      5344 |   25202   122689 |   12197    5302   169868    32.0 |  1.244 % |
c |      5570 |   25202   122689 |   13417    5528   177625    32.1 |  1.244 % |
c ==============================================================================
c (current CPU-time: 19.844 s)
c ==============================================================================
c [1mFound solution: 17414[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5726 |   25256   122855 |    7576    5684   183395    32.3 |  1.244 % |
c   -- subsuming                       
c   -- var.elim.:  108/108          
c   -- var.elim.:  77/77          
c |      5726 |   25232   122984 |      --    5684       --      -- |     --   | -24/130
c |      5726 |   25232   122984 |   10092    5684   183395    32.3 |  1.244 % |
c ==============================================================================
c (current CPU-time: 20.3439 s)
c ==============================================================================
c [1mFound solution: 17413[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5809 |   25297   123206 |    7589    5767   187017    32.4 |  1.244 % |
c   -- subsuming                       
c   -- var.elim.:  153/153          
c   -- var.elim.:  115/115          
c |      5809 |   25265   123337 |      --    5767       --      -- |     --   | -32/132
c |      5809 |   25265   123337 |   10106    5767   187017    32.4 |  1.244 % |
c ==============================================================================
c (current CPU-time: 20.8188 s)
c ==============================================================================
c [1mFound solution: 17412[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5887 |   25330   123552 |    7598    5845   189377    32.4 |  1.244 % |
c   -- subsuming                       
c   -- var.elim.:  146/146          
c   -- var.elim.:  108/108          
c |      5887 |   25298   123683 |      --    5845       --      -- |     --   | -32/132
c |      5887 |   25298   123683 |   10119    5845   189377    32.4 |  1.244 % |
c ==============================================================================
c (current CPU-time: 21.2418 s)
c ==============================================================================
c [1mFound solution: 17410[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5962 |   25360   123883 |    7607    5920   195152    33.0 |  1.244 % |
c   -- subsuming                       
c   -- var.elim.:  134/134          
c   -- var.elim.:  99/99          
c |      5962 |   25331   124020 |      --    5920       --      -- |     --   | -29/138
c |      5962 |   25331   124020 |   10132    5920   195152    33.0 |  1.244 % |
c ==============================================================================
c (current CPU-time: 21.6487 s)
c ==============================================================================
c [1mFound solution: 17409[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6044 |   25394   124221 |    7618    6001   200302    33.4 |  1.244 % |
c   -- subsuming                       
c   -- var.elim.:  277/277          
c   -- var.elim.:  115/115          
c |      6044 |   25362   124361 |      --    6001       --      -- |     --   | -32/141
c |      6044 |   25362   124361 |   10144    6001   200302    33.4 |  1.244 % |
c |      6145 |   25362   124361 |   11159    6102   205638    33.7 |  1.305 % |
c ==============================================================================
c (current CPU-time: 22.1766 s)
c ==============================================================================
c [1mFound solution: 17408[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6174 |   25412   124501 |    7623    6131   207318    33.8 |  1.305 % |
c   -- subsuming                       
c   -- var.elim.:  86/86          
c   -- var.elim.:  57/57          
c |      6174 |   25390   124634 |      --    6131       --      -- |     --   | -22/134
c |      6174 |   25390   124634 |   10156    6128   207293    33.8 |  1.305 % |
c |      6278 |   25390   124634 |   11171    6232   209386    33.6 |  1.315 % |
c |      6429 |   25390   124634 |   12288    6383   215005    33.7 |  1.315 % |
c |      6655 |   25390   124634 |   13517    6609   224815    34.0 |  1.315 % |
c |      6994 |   25390   124634 |   14869    6948   232710    33.5 |  1.315 % |
c |      7502 |   25388   124619 |   16355    7453   262811    35.3 |  1.326 % |
c |      8261 |   25388   124619 |   17990    8212   292506    35.6 |  1.326 % |
c |      9400 |   25388   124619 |   19789    9351   339242    36.3 |  1.326 % |
c |     11108 |   25386   124597 |   21766   11044   421714    38.2 |  1.336 % |
c ==============================================================================
c (current CPU-time: 28.9916 s)
c ==============================================================================
c [1mFound solution: 16426[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     12027 |   25443   124777 |    7632   11963   493838    41.3 |  1.336 % |
c   -- subsuming                       
c   -- var.elim.:  315/315          
c   -- var.elim.:  109/109          
c   -- var.elim.:  136/136          
c   -- var.elim.:  40/40          
c   -- var.elim.:  9/9          
c |     12027 |   24664   116571 |      --   11963       --      -- |     --   | -779/-8205
c |     12027 |   24664   116571 |    9865   10888   446317    41.0 |  1.336 % |
c |     12127 |   24664   116571 |   10852    7359   300160    40.8 |  1.351 % |
c |     12278 |   24664   116571 |   11937    7510   306196    40.8 |  1.351 % |
c |     12503 |   24664   116571 |   13131    7735   313370    40.5 |  1.351 % |
c ==============================================================================
c (current CPU-time: 30.3014 s)
c ==============================================================================
c [1mFound solution: 16424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     12714 |   24729   116779 |    7418    7946   321650    40.5 |  1.351 % |
c   -- subsuming                       
c   -- var.elim.:  139/139          
c   -- var.elim.:  100/100          
c |     12714 |   24698   116944 |      --    7946       --      -- |     --   | -31/166
c |     12714 |   24698   116944 |    9879    7946   321650    40.5 |  1.351 % |
c |     12814 |   24698   116944 |   10867    8046   323646    40.2 |  1.360 % |
c |     12965 |   24698   116944 |   11953    8197   328609    40.1 |  1.360 % |
c ==============================================================================
c (current CPU-time: 31.0643 s)
c ==============================================================================
c [1mFound solution: 16422[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13154 |   24750   117104 |    7424    8386   354086    42.2 |  1.360 % |
c   -- subsuming                       
c   -- var.elim.:  105/105          
c   -- var.elim.:  74/74          
c |     13154 |   24723   117215 |      --    8386       --      -- |     --   | -27/112
c |     13154 |   24723   117215 |    9889    8386   354086    42.2 |  1.360 % |
c |     13254 |   24723   117215 |   10878    8486   355894    41.9 |  1.371 % |
c |     13404 |   24723   117215 |   11965    8636   364555    42.2 |  1.371 % |
c |     13629 |   24723   117215 |   13162    8861   377712    42.6 |  1.371 % |
c |     13966 |   24723   117215 |   14478    9198   421802    45.9 |  1.371 % |
c ==============================================================================
c (current CPU-time: 32.631 s)
c ==============================================================================
c [1mFound solution: 16418[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14086 |   24799   117465 |    7439    9318   429614    46.1 |  1.371 % |
c   -- subsuming                       
c   -- var.elim.:  170/170          
c   -- var.elim.:  123/123          
c |     14086 |   24762   117815 |      --    9318       --      -- |     --   | -37/351
c |     14086 |   24762   117815 |    9904    9318   429614    46.1 |  1.371 % |
c |     14187 |   24762   117815 |   10895    9419   434057    46.1 |  1.381 % |
c |     14337 |   24762   117815 |   11984    9569   447898    46.8 |  1.381 % |
c |     14562 |   24762   117815 |   13183    9794   458340    46.8 |  1.381 % |
c ==============================================================================
c (current CPU-time: 33.7259 s)
c ==============================================================================
c [1mFound solution: 16406[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14603 |   24837   118064 |    7451    9835   461888    47.0 |  1.381 % |
c   -- subsuming                       
c   -- var.elim.:  171/171          
c   -- var.elim.:  123/123          
c |     14603 |   24795   118225 |      --    9835       --      -- |     --   | -42/162
c |     14603 |   24795   118225 |    9918    9835   461888    47.0 |  1.381 % |
c |     14704 |   24795   118225 |   10909    9936   464569    46.8 |  1.391 % |
c |     14854 |   24795   118225 |   12000   10086   471467    46.7 |  1.390 % |
c |     15079 |   24795   118225 |   13200   10311   481408    46.7 |  1.390 % |
c |     15416 |   24795   118225 |   14520   10648   499927    47.0 |  1.390 % |
c ==============================================================================
c (current CPU-time: 35.6056 s)
c ==============================================================================
c [1mFound solution: 16402[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15681 |   24861   118451 |    7458   10913   526451    48.2 |  1.390 % |
c   -- subsuming                       
c   -- var.elim.:  156/156          
c   -- var.elim.:  117/117          
c |     15681 |   24827   118593 |      --   10913       --      -- |     --   | -34/143
c |     15681 |   24827   118593 |    9930   10913   526451    48.2 |  1.390 % |
c ==============================================================================
c (current CPU-time: 36.1925 s)
c ==============================================================================
c [1mFound solution: 16398[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15774 |   24893   118819 |    7467    7369   371803    50.5 |  1.390 % |
c   -- subsuming                       
c   -- var.elim.:  156/156          
c   -- var.elim.:  117/117          
c |     15774 |   24859   118943 |      --    7369       --      -- |     --   | -34/125
c |     15774 |   24859   118943 |    9943    7369   371803    50.5 |  1.390 % |
c |     15875 |   24859   118943 |   10937    7470   382171    51.2 |  1.410 % |
c ==============================================================================
c (current CPU-time: 36.7694 s)
c ==============================================================================
c [1mFound solution: 16394[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15968 |   24916   119122 |    7474    7563   388449    51.4 |  1.410 % |
c   -- subsuming                       
c   -- var.elim.:  118/118          
c   -- var.elim.:  86/86          
c |     15968 |   24891   119271 |      --    7563       --      -- |     --   | -25/150
c |     15968 |   24891   119271 |    9956    7563   388449    51.4 |  1.410 % |
c |     16068 |   24891   119271 |   10952    7663   393222    51.3 |  1.420 % |
c |     16218 |   24891   119271 |   12047    7813   400391    51.2 |  1.420 % |
c |     16444 |   24891   119271 |   13251    8039   406395    50.6 |  1.420 % |
c |     16782 |   24891   119271 |   14577    8377   457504    54.6 |  1.420 % |
c ==============================================================================
c (current CPU-time: 38.7601 s)
c ==============================================================================
c [1mFound solution: 16392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17212 |   24948   119450 |    7484    8807   496083    56.3 |  1.420 % |
c   -- subsuming                       
c   -- var.elim.:  119/119          
c   -- var.elim.:  86/86          
c |     17212 |   24921   119588 |      --    8807       --      -- |     --   | -27/139
c |     17212 |   24921   119588 |    9968    8807   496083    56.3 |  1.420 % |
c |     17314 |   24921   119588 |   10965    8909   501195    56.3 |  1.431 % |
c ==============================================================================
c (current CPU-time: 39.432 s)
c ==============================================================================
c [1mFound solution: 16390[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17377 |   24973   119747 |    7491    8972   506032    56.4 |  1.431 % |
c   -- subsuming                       
c   -- var.elim.:  104/104          
c   -- var.elim.:  73/73          
c |     17377 |   24947   119860 |      --    8972       --      -- |     --   | -26/114
c |     17377 |   24947   119860 |    9978    8972   506032    56.4 |  1.431 % |
c |     17478 |   24947   119860 |   10976    9073   508232    56.0 |  1.441 % |
c |     17628 |   24947   119860 |   12074    9223   516598    56.0 |  1.441 % |
c |     17854 |   24947   119860 |   13281    9449   532785    56.4 |  1.441 % |
c |     18192 |   24947   119860 |   14609    9787   563770    57.6 |  1.441 % |
c |     18698 |   24947   119860 |   16070   10293   595013    57.8 |  1.441 % |
c ==============================================================================
c (current CPU-time: 41.8726 s)
c ==============================================================================
c [1mFound solution: 16389[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     18806 |   25010   120075 |    7502   10401   604948    58.2 |  1.441 % |
c   -- subsuming                       
c   -- var.elim.:  148/148          
c   -- var.elim.:  111/111          
c |     18806 |   24978   120201 |      --   10401       --      -- |     --   | -32/127
c |     18806 |   24978   120201 |    9991   10401   604948    58.2 |  1.441 % |
c |     18906 |   24978   120201 |   10990    7034   397038    56.4 |  1.451 % |
c |     19056 |   24978   120201 |   12089    7184   403074    56.1 |  1.451 % |
c |     19281 |   24978   120201 |   13298    7409   425471    57.4 |  1.451 % |
c ==============================================================================
c (current CPU-time: 43.1444 s)
c ==============================================================================
c [1mFound solution: 16386[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19380 |   25039   120396 |    7511    7508   431010    57.4 |  1.451 % |
c   -- subsuming                       
c   -- var.elim.:  130/130          
c   -- var.elim.:  95/95          
c |     19380 |   25009   120526 |      --    7508       --      -- |     --   | -30/131
c |     19380 |   25009   120526 |   10003    7508   431010    57.4 |  1.451 % |
c ==============================================================================
c (current CPU-time: 43.6974 s)
c ==============================================================================
c [1mFound solution: 16385[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19464 |   25073   120742 |    7521    7592   434682    57.3 |  1.451 % |
c   -- subsuming                       
c   -- var.elim.:  148/148          
c   -- var.elim.:  111/111          
c |     19464 |   25041   120877 |      --    7592       --      -- |     --   | -32/136
c |     19464 |   25041   120877 |   10016    7592   434682    57.3 |  1.451 % |
c ==============================================================================
c (current CPU-time: 44.1653 s)
c ==============================================================================
c [1mFound solution: 16384[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19512 |   25089   121010 |    7526    7640   441435    57.8 |  1.451 % |
c   -- subsuming                       
c   -- var.elim.:  81/81          
c   -- var.elim.:  53/53          
c |     19512 |   25067   121138 |      --    7640       --      -- |     --   | -22/129
c |     19512 |   25067   121138 |   10026    7640   441435    57.8 |  1.451 % |
c |     19613 |   25067   121138 |   11029    7741   443308    57.3 |  1.481 % |
c |     19763 |   25067   121138 |   12132    7891   450629    57.1 |  1.481 % |
c |     19991 |   25067   121138 |   13345    8119   453764    55.9 |  1.481 % |
c |     20329 |   25067   121138 |   14680    8457   476614    56.4 |  1.481 % |
c |     20837 |   25067   121138 |   16148    8965   520602    58.1 |  1.481 % |
c |     21599 |   25061   121084 |   17758    9572   557165    58.2 |  1.512 % |
c |     22739 |   25061   121084 |   19534   10712   659415    61.6 |  1.512 % |
c |     24447 |   25061   121084 |   21488   12420   789835    63.6 |  1.512 % |
c |     27010 |   25061   121084 |   23637   14983  1055549    70.4 |  1.512 % |
c |     30854 |   25061   121084 |   26000   18827  1392987    74.0 |  1.512 % |
c |     36620 |   25061   121084 |   28600   24593  1788058    72.7 |  1.512 % |
c |     45269 |   25061   121084 |   31460   17420  1455778    83.6 |  1.512 % |
c |     58243 |   25057   121065 |   34601   30392  2711083    89.2 |  1.533 % |
c ==============================================================================
c (current CPU-time: 102.887 s)
c ==============================================================================
c [1mFound solution: 16378[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     70520 |   25112   121233 |    7533   23301  1648893    70.8 |  1.533 % |
c   -- subsuming                       
c   -- var.elim.:  354/354          
c   -- var.elim.:  94/94          
c |     70520 |   25088   121387 |      --   23301       --      -- |     --   | -24/155
c |     70520 |   25088   121387 |   10035   23301  1648893    70.8 |  1.533 % |
c |     70621 |   25088   121387 |   11038   10043   510497    50.8 |  1.553 % |
c |     70773 |   25088   121387 |   12142   10195   515137    50.5 |  1.553 % |
c |     70998 |   25079   121249 |   13352   10394   518441    49.9 |  1.574 % |
c |     71335 |   25073   121195 |   14683   10730   540553    50.4 |  1.605 % |
c |     71841 |   25073   121195 |   16152   11236   572189    50.9 |  1.605 % |
c |     72600 |   25009   120386 |   17721   11607   588221    50.7 |  1.791 % |
c |     73740 |   25009   120386 |   19494   12747   643008    50.4 |  1.791 % |
c |     75450 |   25009   120386 |   21443   14457   743365    51.4 |  1.791 % |
c |     78012 |   25009   120386 |   23587   17019  1133452    66.6 |  1.791 % |
c |     81857 |   25009   120386 |   25946   20864  1458324    69.9 |  1.791 % |
c ==============================================================================
c (current CPU-time: 119.303 s)
c ==============================================================================
c [1mFound solution: 16375[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     82147 |   25031   120439 |    7509   21154  1480532    70.0 |  1.791 % |
c   -- subsuming                       
c   -- var.elim.:  702/702          
c   -- var.elim.:  303/303          
c   -- var.elim.:  197/197          
c   -- var.elim.:  211/211          
c |     82147 |   24997   120904 |      --   21154       --      -- |     --   | -34/466
c |     82147 |   24997   120904 |    9998   20030  1240079    61.9 |  1.791 % |
c |     82247 |   24997   120904 |   10998    9003   654543    72.7 |  1.835 % |
c |     82397 |   24997   120904 |   12098    9153   664517    72.6 |  1.835 % |
c |     82622 |   24997   120904 |   13308    9378   685748    73.1 |  1.835 % |
c |     82959 |   24997   120904 |   14639    9715   708526    72.9 |  1.835 % |
c |     83465 |   24997   120904 |   16103   10221   745268    72.9 |  1.835 % |
c |     84227 |   24997   120904 |   17713   10983   799352    72.8 |  1.835 % |
c |     85366 |   24991   120856 |   19480   12039   920660    76.5 |  1.866 % |
c |     87075 |   24991   120856 |   21428   13748  1062830    77.3 |  1.866 % |
c |     89637 |   24991   120856 |   23570   16310  1235492    75.8 |  1.866 % |
c |     93482 |   24991   120856 |   25928   20155  1582590    78.5 |  1.866 % |
c |     99248 |   24991   120856 |   28520   25921  2157013    83.2 |  1.866 % |
c ==============================================================================
c (current CPU-time: 147.721 s)
c ==============================================================================
c [1mFound solution: 16374[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    102259 |   25053   121081 |    7515   28932  2428833    83.9 |  1.866 % |
c   -- subsuming                       
c   -- var.elim.:  516/516          
c   -- var.elim.:  127/127          
c |    102259 |   25018   122190 |      --   28932       --      -- |     --   | -35/1110
c |    102259 |   25018   122190 |   10007   28895  2421192    83.8 |  1.866 % |
c |    102362 |   25018   122190 |   11007    6970   397839    57.1 |  1.876 % |
c |    102512 |   25018   122190 |   12108    7120   406093    57.0 |  1.876 % |
c |    102738 |   25018   122190 |   13319    7346   420089    57.2 |  1.876 % |
c |    103076 |   25018   122190 |   14651    7684   448182    58.3 |  1.876 % |
c |    103582 |   25018   122190 |   16116    8190   480835    58.7 |  1.876 % |
c |    104341 |   25018   122190 |   17728    8949   548548    61.3 |  1.876 % |
c |    105482 |   25018   122190 |   19501   10090   594654    58.9 |  1.876 % |
c |    107190 |   25018   122190 |   21451   11798   738740    62.6 |  1.876 % |
c |    109753 |   25018   122190 |   23596   14361   982765    68.4 |  1.876 % |
c |    113599 |   25018   122190 |   25956   18207  1591865    87.4 |  1.876 % |
c |    119366 |   25018   122190 |   28551   23974  2161096    90.1 |  1.876 % |
c |    128015 |   25018   122190 |   31406   16221  1143919    70.5 |  1.876 % |
c |    140989 |   25003   121365 |   34526   29194  2329439    79.8 |  1.886 % |
c |    160450 |   25003   121365 |   37979   28135  3236599   115.0 |  1.886 % |
c |    189643 |   25003   121365 |   41777   31988  5555883   173.7 |  1.886 % |
c ==============================================================================
c (current CPU-time: 273.974 s)
c ==============================================================================
c [1mFound solution: 16373[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    193667 |   25050   121555 |    7514   36012  6000037   166.6 |  1.886 % |
c   -- subsuming                       
c   -- var.elim.:  363/363          
c   -- var.elim.:  345/345          
c |    193667 |   24999   121977 |      --   36012       --      -- |     --   | -51/423
c |    193667 |   24999   121977 |    9999   36012  6000037   166.6 |  1.886 % |
c |    193767 |   24999   121977 |   10999   10239   821445    80.2 |  1.897 % |
c |    193918 |   24999   121977 |   12099   10390   826843    79.6 |  1.897 % |
c |    194143 |   24999   121977 |   13309   10615   834225    78.6 |  1.897 % |
c |    194480 |   24999   121977 |   14640   10952   855711    78.1 |  1.898 % |
c |    194986 |   24999   121977 |   16104   11458   908361    79.3 |  1.897 % |
c |    195745 |   24999   121977 |   17714   12217   986642    80.8 |  1.897 % |
c |    196886 |   24870   120531 |   19385   13327  1163267    87.3 |  2.374 % |
c |    198594 |   24854   120438 |   21310   15031  1341674    89.3 |  2.457 % |
c |    201159 |   24854   120438 |   23441   17596  1620250    92.1 |  2.457 % |
c |    205003 |   24838   120344 |   25769   21436  1978735    92.3 |  2.540 % |
c |    210769 |   24838   120344 |   28346   27202  2434421    89.5 |  2.540 % |
c |    219418 |   24832   120292 |   31173   17665  2462284   139.4 |  2.571 % |
c |    232392 |   24832   120292 |   34290   30639  4069297   132.8 |  2.571 % |
c |    251855 |   24832   120292 |   37719   29286  3035479   103.6 |  2.571 % |
c ==============================================================================
c (current CPU-time: 355.093 s)
c ==============================================================================
c [1mFound solution: 16368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    254163 |   24877   120462 |    7463   31594  3200227   101.3 |  2.571 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1629          
c   -- var.elim.:  1629/1629          
c   -- var.elim.:  326/326          
c   -- var.elim.:  230/230          
c   -- var.elim.:  128/128          
c   -- subsuming                       
c   -- var.elim.:  256/256          
c   -- var.elim.:  153/153          
c |    254163 |   24801   121436 |      --   31594       --      -- |     --   | -76/975
c |    254163 |   24801   121436 |    9920   29980  2470663    82.4 |  2.571 % |
c |    254264 |   24801   121436 |   10912    9597   464298    48.4 |  2.590 % |
c |    254416 |   24801   121436 |   12003    9749   468816    48.1 |  2.590 % |
c |    254641 |   24801   121436 |   13204    9974   474408    47.6 |  2.590 % |
c |    254978 |   24801   121436 |   14524   10311   485314    47.1 |  2.590 % |
c |    255484 |   24801   121436 |   15976   10817   503831    46.6 |  2.590 % |
c |    256243 |   24737   120415 |   17529   11298   520556    46.1 |  2.757 % |
c |    257384 |   24737   120415 |   19282   12439   577306    46.4 |  2.757 % |
c |    259092 |   24737   120415 |   21210   14147   646592    45.7 |  2.757 % |
c |    261654 |   24737   120415 |   23331   16709   909547    54.4 |  2.757 % |
c |    265498 |   24721   120321 |   25647   20551  1222374    59.5 |  2.840 % |
c |    271264 |   24721   120321 |   28212   26317  1947068    74.0 |  2.840 % |
c |    279913 |   24721   120321 |   31034   19671  1887334    95.9 |  2.840 % |
c ==============================================================================
c (current CPU-time: 393.595 s)
c ==============================================================================
c [1mFound solution: 16367[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    284022 |   24765   120488 |    7429   23780  2229501    93.8 |  2.840 % |
c   -- subsuming                       
c   -- var.elim.:  713/713          
c   -- var.elim.:  376/376          
c   -- var.elim.:  162/162          
c   -- var.elim.:  241/241          
c |    284022 |   24684   119200 |      --   23780       --      -- |     --   | -81/-1287
c |    284022 |   24684   119200 |    9873   23245  2175023    93.6 |  2.840 % |
c |    284123 |   24684   119200 |   10860    9735   748673    76.9 |  2.856 % |
c |    284274 |   24684   119200 |   11947    9886   753183    76.2 |  2.856 % |
c |    284499 |   24684   119200 |   13141   10111   768696    76.0 |  2.856 % |
c |    284838 |   24684   119200 |   14455   10450   787526    75.4 |  2.856 % |
c |    285345 |   24684   119200 |   15901   10957   823035    75.1 |  2.856 % |
c |    286105 |   24684   119200 |   17491   11717   875930    74.8 |  2.856 % |
c |    287244 |   24684   119200 |   19240   12856   996169    77.5 |  2.856 % |
c |    288953 |   24684   119200 |   21164   14565  1090984    74.9 |  2.856 % |
c |    291517 |   24684   119200 |   23281   17129  1363343    79.6 |  2.856 % |
c |    295361 |   24684   119200 |   25609   20973  1700162    81.1 |  2.856 % |
c |    301131 |   24668   119106 |   28152   26742  2294555    85.8 |  2.940 % |
c |    309780 |   24668   119106 |   30967   18302  1308196    71.5 |  2.939 % |
c |    322757 |   24668   119106 |   34064   31279  3089788    98.8 |  2.940 % |
c |    342221 |   24668   119106 |   37470   30845  4688950   152.0 |  2.940 % |
c |    371415 |   24658   119073 |   41201   36633  6474726   176.7 |  2.960 % |
c |    415205 |   24658   119073 |   45321   22972  7231878   314.8 |  2.960 % |
c |    480889 |   24658   119073 |   49853   21471  6138707   285.9 |  2.960 % |
c |    579421 |   24658   119073 |   54838   43565 11227295   257.7 |  2.960 % |
c ==============================================================================
c (current CPU-time: 920.509 s)
c ==============================================================================
c [1mFound solution: 16295[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    588699 |   24703   119232 |    7410   52843 12666398   239.7 |  2.960 % |
c   -- subsuming                       
c   -- var.elim.:  511/511          
c   -- var.elim.:  87/87          
c |    588699 |   24676   119585 |      --   52843       --      -- |     --   | -27/354
c |    588699 |   24676   119585 |    9870   52843 12666398   239.7 |  2.960 % |
c |    588799 |   24676   119585 |   10857   10061  1373717   136.5 |  2.970 % |
c |    588950 |   24676   119585 |   11943   10212  1378063   134.9 |  2.970 % |
c |    589176 |   24676   119585 |   13137   10438  1396636   133.8 |  2.970 % |
c |    589513 |   24676   119585 |   14451   10775  1410617   130.9 |  2.970 % |
c |    590020 |   24676   119585 |   15896   11282  1443485   127.9 |  2.970 % |
c |    590781 |   24676   119585 |   17486   12043  1509134   125.3 |  2.970 % |
c |    591920 |   24676   119585 |   19234   13182  1627150   123.4 |  2.970 % |
c |    593628 |   24676   119585 |   21158   14890  1786837   120.0 |  2.970 % |
c ==============================================================================
c (current CPU-time: 931.91 s)
c ==============================================================================
c [1mFound solution: 16278[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    595751 |   24729   119790 |    7418   17013  1878122   110.4 |  2.970 % |
c   -- subsuming                       
c   -- var.elim.:  150/150          
c   -- var.elim.:  113/113          
c |    595751 |   24695   120201 |      --   17013       --      -- |     --   | -34/412
c |    595751 |   24695   120201 |    9878   17013  1878122   110.4 |  2.970 % |
c |    595851 |   24695   120201 |   10865    7663   437024    57.0 |  2.980 % |
c |    596001 |   24695   120201 |   11952    7813   446642    57.2 |  2.980 % |
c |    596227 |   24695   120201 |   13147    8039   463338    57.6 |  2.980 % |
c |    596565 |   24695   120201 |   14462    8377   502072    59.9 |  2.980 % |
c |    597072 |   24695   120201 |   15908    8884   548795    61.8 |  2.980 % |
c |    597831 |   24695   120201 |   17499    9643   629666    65.3 |  2.980 % |
c |    598970 |   24695   120201 |   19249   10782   750232    69.6 |  2.980 % |
c |    600679 |   24695   120201 |   21174   12491   864476    69.2 |  2.980 % |
c |    603241 |   24695   120201 |   23291   15053  1113925    74.0 |  2.980 % |
c |    607086 |   24695   120201 |   25620   18898  1470213    77.8 |  2.980 % |
c |    612854 |   24695   120201 |   28183   24666  2320192    94.1 |  2.980 % |
c |    621503 |   24695   120201 |   31001   18592  2030610   109.2 |  2.980 % |
c ==============================================================================
c (current CPU-time: 977.189 s)
c ==============================================================================
c [1mFound solution: 16102[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    629173 |   24732   120296 |    7419   26262  2796123   106.5 |  2.980 % |
c   -- subsuming                       
c   -- var.elim.:  56/56          
c   -- var.elim.:  32/32          
c |    629173 |   24711   120433 |      --   26262       --      -- |     --   | -21/138
c |    629173 |   24711   120433 |    9884   26262  2796123   106.5 |  2.980 % |
c |    629274 |   24711   120433 |   10872    7002   502126    71.7 |  2.990 % |
c |    629425 |   24711   120433 |   11960    7153   507773    71.0 |  2.990 % |
c |    629650 |   24711   120433 |   13156    7378   518494    70.3 |  2.990 % |
c |    629987 |   24711   120433 |   14471    7715   536038    69.5 |  2.990 % |
c |    630494 |   24711   120433 |   15918    8222   569489    69.3 |  2.990 % |
c |    631253 |   24711   120433 |   17510    8981   656421    73.1 |  2.990 % |
c |    632392 |   24711   120433 |   19261   10120   766386    75.7 |  2.990 % |
c |    634101 |   24711   120433 |   21188   11829  1013351    85.7 |  2.990 % |
c |    636663 |   24711   120433 |   23306   14391  1286216    89.4 |  2.990 % |
c |    640507 |   24711   120433 |   25637   18235  1776256    97.4 |  2.990 % |
c |    646277 |   24711   120433 |   28201   24005  2657452   110.7 |  2.990 % |
c |    654926 |   24711   120433 |   31021   18091  2263081   125.1 |  2.990 % |
c |    667903 |   24711   120433 |   34123   31068  6794448   218.7 |  2.990 % |
c ==============================================================================
c (current CPU-time: 1058.77 s)
c ==============================================================================
c [1mFound solution: 16098[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    674828 |   24761   120611 |    7428   37993  7481639   196.9 |  2.990 % |
c   -- subsuming                       
c   -- var.elim.:  126/126          
c   -- var.elim.:  92/92          
c |    674828 |   24730   120758 |      --   37993       --      -- |     --   | -31/148
c |    674828 |   24730   120758 |    9892   37993  7481639   196.9 |  2.990 % |
c |    674930 |   24730   120758 |   10881    7297   495069    67.8 |  3.000 % |
c |    675080 |   24730   120758 |   11969    7447   512526    68.8 |  3.000 % |
c |    675305 |   24730   120758 |   13166    7672   522117    68.1 |  3.000 % |
c |    675645 |   24730   120758 |   14482    8012   557170    69.5 |  3.000 % |
c |    676152 |   24730   120758 |   15931    8519   585124    68.7 |  3.000 % |
c |    676913 |   24730   120758 |   17524    9280   632062    68.1 |  3.000 % |
c |    678052 |   24730   120758 |   19276   10419   773694    74.3 |  3.000 % |
c |    679760 |   24730   120758 |   21204   12127  1061488    87.5 |  3.000 % |
c |    682322 |   24714   120478 |   23309   14686  1329737    90.5 |  3.021 % |
c |    686168 |   24714   120478 |   25640   18532  1872215   101.0 |  3.021 % |
c |    691935 |   24714   120478 |   28204   24299  2795470   115.0 |  3.021 % |
c |    700584 |   24714   120478 |   31025   18539  2146066   115.8 |  3.021 % |
c |    713558 |   24714   120478 |   34127   31513  3832745   121.6 |  3.021 % |
c |    733019 |   24714   120478 |   37540   31834  4268406   134.1 |  3.021 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -d1_bit0 -d2_bit0 -d3_bit0 -d4_bit0 -d5_bit0 -d6_bit0 -d7_bit0 -d8_bit0 -d9_bit0 -d10_bit0 d11_bit0 d12_bit0 d13_bit0 d14_bit0 -d15_bit0#### 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.70 0.90 0.89 2/54 15047
Raw data (stat): 15047 (runsolver) R 15046 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548292885 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99942 s]
Raw data (loadavg): 0.75 0.90 0.89 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 7620 0 0 0 970 27 0 0 25 0 1 0 548292885 18595840 3719 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4540 3719 603 41 0 4499 0
vsize: 18160
[startup+20.0001 s]
Raw data (loadavg): 0.78 0.90 0.89 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 16823 0 0 0 1931 66 0 0 25 0 1 0 548292885 19566592 3973 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4777 3973 603 41 0 4736 0
vsize: 19108
[startup+30.0007 s]
Raw data (loadavg): 0.82 0.91 0.89 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 20388 0 0 0 2914 82 0 0 25 0 1 0 548292885 22343680 4539 4294967295 134512640 134672761 3221224544 3221222880 134605508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5455 4539 603 41 0 5414 0
vsize: 21820
[startup+40.0012 s]
Raw data (loadavg): 0.84 0.91 0.89 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 24694 0 0 0 3896 100 0 0 25 0 1 0 548292885 22769664 4650 4294967295 134512640 134672761 3221224544 3221222808 1075730078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5559 4650 603 41 0 5518 0
vsize: 22236
[startup+50.0019 s]
Raw data (loadavg): 0.87 0.91 0.89 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 26836 0 0 0 4885 111 0 0 25 0 1 0 548292885 20873216 4378 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5096 4378 603 41 0 5055 0
vsize: 20384
[startup+60.0017 s]
Raw data (loadavg): 0.89 0.91 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 27276 0 0 0 5884 112 0 0 25 0 1 0 548292885 22773760 4818 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5560 4818 603 41 0 5519 0
vsize: 22240
[startup+70.002 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 28222 0 0 0 6881 115 0 0 25 0 1 0 548292885 26587136 5764 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6491 5764 603 41 0 6450 0
vsize: 25964
[startup+80.0016 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 28297 0 0 0 7882 115 0 0 25 0 1 0 548292885 26869760 5839 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6560 5839 603 41 0 6519 0
vsize: 26240
[startup+90.0025 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 28584 0 0 0 8881 116 0 0 25 0 1 0 548292885 28049408 6126 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6848 6126 603 41 0 6807 0
vsize: 27392
[startup+100.002 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 29261 0 0 0 9879 118 0 0 25 0 1 0 548292885 31211520 6803 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7620 6803 603 41 0 7579 0
vsize: 30480
[startup+110.002 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 29965 0 0 0 10875 121 0 0 25 0 1 0 548292885 32587776 7125 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7956 7125 603 41 0 7915 0
vsize: 31824
[startup+120.002 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 29965 0 0 0 11875 121 0 0 25 0 1 0 548292885 32587776 7125 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7956 7125 603 41 0 7915 0
vsize: 31824
[startup+130.002 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30350 0 0 0 12874 123 0 0 25 0 1 0 548292885 32489472 7175 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7932 7175 603 41 0 7891 0
vsize: 31728
[startup+140.002 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30350 0 0 0 13874 123 0 0 25 0 1 0 548292885 32489472 7175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7932 7175 603 41 0 7891 0
vsize: 31728
[startup+150.003 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30710 0 0 0 14872 125 0 0 25 0 1 0 548292885 31211520 6871 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7620 6871 603 41 0 7579 0
vsize: 30480
[startup+160.002 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 15871 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7620 6873 603 41 0 7579 0
vsize: 30480
[startup+170.002 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 16872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7620 6873 603 41 0 7579 0
vsize: 30480
[startup+180.002 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 17872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223584 134612827 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7620 6873 603 41 0 7579 0
vsize: 30480
[startup+190.002 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 18872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7620 6873 603 41 0 7579 0
vsize: 30480
[startup+200.002 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 19872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223536 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7620 6873 603 41 0 7579 0
vsize: 30480
[startup+210.002 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30747 0 0 0 20872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7620 6873 603 41 0 7579 0
vsize: 30480
[startup+220.002 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30747 0 0 0 21872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7620 6873 603 41 0 7579 0
vsize: 30480
[startup+230.002 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 31746 0 0 0 22869 128 0 0 25 0 1 0 548292885 35414016 7872 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 7872 603 41 0 8605 0
vsize: 34584
[startup+240.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 33596 0 0 0 23864 134 0 0 25 0 1 0 548292885 42987520 9722 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10495 9722 603 41 0 10454 0
vsize: 41980
[startup+250.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35065 0 0 0 24861 137 0 0 25 0 1 0 548292885 48726016 11152 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11896 11152 603 41 0 11855 0
vsize: 47584
[startup+260.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35065 0 0 0 25861 137 0 0 25 0 1 0 548292885 48726016 11152 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11896 11152 603 41 0 11855 0
vsize: 47584
[startup+270.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35065 0 0 0 26861 137 0 0 25 0 1 0 548292885 48726016 11152 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11896 11152 603 41 0 11855 0
vsize: 47584
[startup+280.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 27857 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11441 603 41 0 12203 0
vsize: 48976
[startup+290.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 28858 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11441 603 41 0 12203 0
vsize: 48976
[startup+300.111 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 29868 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11441 603 41 0 12203 0
vsize: 48976
[startup+310.113 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 30869 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11441 603 41 0 12203 0
vsize: 48976
[startup+320.121 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 31870 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11441 603 41 0 12203 0
vsize: 48976
[startup+330.122 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 32870 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11441 603 41 0 12203 0
vsize: 48976
[startup+340.122 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 33870 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11441 603 41 0 12203 0
vsize: 48976
[startup+350.121 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 34870 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11441 603 41 0 12203 0
vsize: 48976
[startup+360.121 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35915 0 0 0 35869 141 0 0 25 0 1 0 548292885 48648192 11135 4294967295 134512640 134672761 3221224544 3221223728 134615985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11877 11135 603 41 0 11836 0
vsize: 47508
[startup+370.121 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35915 0 0 0 36868 141 0 0 25 0 1 0 548292885 48648192 11135 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11135 603 41 0 11836 0
vsize: 47508
[startup+380.121 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35915 0 0 0 37869 141 0 0 25 0 1 0 548292885 48648192 11135 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11135 603 41 0 11836 0
vsize: 47508
[startup+390.122 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35915 0 0 0 38869 141 0 0 25 0 1 0 548292885 48648192 11135 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11135 603 41 0 11836 0
vsize: 47508
[startup+400.121 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 39867 143 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+410.12 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 40867 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+420.122 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 41867 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+430.122 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 42867 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+440.122 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 43868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+450.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 44868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+460.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 45868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+470.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 46868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+480.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 47868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+490.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 48868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+500.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 49869 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+510.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 50870 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+520.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 51870 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11877 11137 603 41 0 11836 0
vsize: 47508
[startup+530.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36819 0 0 0 52868 146 0 0 25 0 1 0 548292885 50962432 11707 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12442 11707 603 41 0 12401 0
vsize: 49768
[startup+540.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36819 0 0 0 53869 146 0 0 25 0 1 0 548292885 50962432 11707 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12442 11707 603 41 0 12401 0
vsize: 49768
[startup+550.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36819 0 0 0 54869 146 0 0 25 0 1 0 548292885 50962432 11707 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12442 11707 603 41 0 12401 0
vsize: 49768
[startup+560.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36819 0 0 0 55869 146 0 0 25 0 1 0 548292885 50962432 11707 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12442 11707 603 41 0 12401 0
vsize: 49768
[startup+570.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 37132 0 0 0 56868 147 0 0 25 0 1 0 548292885 52281344 12020 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12764 12020 603 41 0 12723 0
vsize: 51056
[startup+580.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 38454 0 0 0 57865 150 0 0 25 0 1 0 548292885 57761792 13342 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14102 13342 603 41 0 14061 0
vsize: 56408
[startup+590.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 58861 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15329 14592 603 41 0 15288 0
vsize: 61316
[startup+600.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 59861 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15329 14592 603 41 0 15288 0
vsize: 61316
[startup+610.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 60862 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15329 14592 603 41 0 15288 0
vsize: 61316
[startup+620.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 61862 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15329 14592 603 41 0 15288 0
vsize: 61316
[startup+630.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 62862 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15329 14592 603 41 0 15288 0
vsize: 61316
[startup+640.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 63862 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15307 14573 603 41 0 15266 0
vsize: 61228
[startup+650.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 64862 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15307 14573 603 41 0 15266 0
vsize: 61228
[startup+660.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 65863 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15307 14573 603 41 0 15266 0
vsize: 61228
[startup+670.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 66863 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223584 134614239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15307 14573 603 41 0 15266 0
vsize: 61228
[startup+680.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 67863 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15307 14573 603 41 0 15266 0
vsize: 61228
[startup+690.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39802 0 0 0 68863 154 0 0 25 0 1 0 548292885 62693376 14575 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15306 14575 603 41 0 15265 0
vsize: 61224
[startup+700.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39802 0 0 0 69864 154 0 0 25 0 1 0 548292885 62693376 14575 4294967295 134512640 134672761 3221224544 3221223680 134614685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15306 14575 603 41 0 15265 0
vsize: 61224
[startup+710.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39802 0 0 0 70864 154 0 0 25 0 1 0 548292885 62693376 14575 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15306 14575 603 41 0 15265 0
vsize: 61224
[startup+720.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39802 0 0 0 71864 154 0 0 25 0 1 0 548292885 62693376 14575 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15306 14575 603 41 0 15265 0
vsize: 61224
[startup+730.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 40595 0 0 0 72863 156 0 0 25 0 1 0 548292885 65970176 15368 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16106 15368 603 41 0 16065 0
vsize: 64424
[startup+740.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 42100 0 0 0 73859 160 0 0 25 0 1 0 548292885 72142848 16873 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17613 16873 603 41 0 17572 0
vsize: 70452
[startup+750.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 43629 0 0 0 74856 162 0 0 25 0 1 0 548292885 78422016 18402 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19146 18402 603 41 0 19105 0
vsize: 76584
[startup+760.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45366 0 0 0 75852 167 0 0 25 0 1 0 548292885 85594112 20139 4294967295 134512640 134672761 3221224544 3221223552 134522369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20897 20139 603 41 0 20856 0
vsize: 83588
[startup+770.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 76851 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20342 603 41 0 21030 0
vsize: 84284
[startup+780.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 77851 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20342 603 41 0 21030 0
vsize: 84284
[startup+790.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 78852 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20342 603 41 0 21030 0
vsize: 84284
[startup+800.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 79852 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20342 603 41 0 21030 0
vsize: 84284
[startup+810.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 80852 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20342 603 41 0 21030 0
vsize: 84284
[startup+820.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 81852 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20342 603 41 0 21030 0
vsize: 84284
[startup+830.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45593 0 0 0 82852 168 0 0 25 0 1 0 548292885 86306816 20343 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20343 603 41 0 21030 0
vsize: 84284
[startup+840.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 46298 0 0 0 83851 170 0 0 25 0 1 0 548292885 89194496 21048 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21776 21048 603 41 0 21735 0
vsize: 87104
[startup+850.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 47724 0 0 0 84847 174 0 0 25 0 1 0 548292885 95076352 22474 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23212 22474 603 41 0 23171 0
vsize: 92848
[startup+860.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49190 0 0 0 85842 179 0 0 25 0 1 0 548292885 101126144 23940 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24689 23940 603 41 0 24648 0
vsize: 98756
[startup+870.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 86842 179 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25004 24271 603 41 0 24963 0
vsize: 100016
[startup+880.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 87842 179 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25004 24271 603 41 0 24963 0
vsize: 100016
[startup+890.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 88842 179 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25004 24271 603 41 0 24963 0
vsize: 100016
[startup+900.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 89842 179 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25004 24271 603 41 0 24963 0
vsize: 100016
[startup+910.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 90842 180 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25004 24271 603 41 0 24963 0
vsize: 100016
[startup+920.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 91842 180 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25004 24271 603 41 0 24963 0
vsize: 100016
[startup+930.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 92839 182 0 0 25 0 1 0 548292885 102334464 24255 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24984 24255 603 41 0 24943 0
vsize: 99936
[startup+940.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 93838 183 0 0 25 0 1 0 548292885 102313984 24250 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24250 603 41 0 24938 0
vsize: 99916
[startup+950.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 94838 183 0 0 25 0 1 0 548292885 102313984 24250 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24250 603 41 0 24938 0
vsize: 99916
[startup+960.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 95838 183 0 0 25 0 1 0 548292885 102313984 24250 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24250 603 41 0 24938 0
vsize: 99916
[startup+970.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 96838 184 0 0 25 0 1 0 548292885 102313984 24250 4294967295 134512640 134672761 3221224544 3221223584 134614340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24250 603 41 0 24938 0
vsize: 99916
[startup+980.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 97837 184 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223640 134616108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+990.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 98837 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1000.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 99837 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1010.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 100837 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1020.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 101837 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1030.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 102838 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1040.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 103838 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1050.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 104838 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1060.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 105838 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1070.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 106836 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1080.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 107836 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1090.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 108837 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223552 134542729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1100.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 109837 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1110.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 110838 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1120.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 111838 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1130.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 112839 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223640 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1140.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 113839 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1150.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 114840 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1160.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 115840 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1170.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 116841 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223584 134614286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1180.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 117841 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 118841 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15047
Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 119841 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24979 24251 603 41 0 24938 0
vsize: 99916
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 15047
Raw data (stat): 15047 (minisat+) Z 15046 28099 28098 0 -1 12 49868 0 0 0 119842 191 0 0 25 0 1 0 548292885 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.22
CPU time (s): 1200.34
CPU user time (s): 1198.42
CPU system time (s): 1.91671
CPU usage (%): 100.01
Max. virtual memory (Kb): 100016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####