PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-egout.opb
MD5SUM	46c4db5f8baf54496e00a723c85beb20
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	58880896
Optimality of the best value was proved	NO
Number of terms in the objective function	1095
Biggest coefficient in the objective function	533200896
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	14929722305
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	533200896
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	14929722305
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	1155
Total number of constraints	153
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	98
Minimum length of a constraint	1
Maximum length of a constraint	280
Trace number 19260

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 18:30:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16794 boxname=wulflinc30 idbench=1292 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  46c4db5f8baf54496e00a723c85beb20  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-egout.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-egout.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-egout.opb
IDLAUNCH: 16794
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        840224 kB
Buffers:         13872 kB
Cached:         153924 kB
SwapCached:         28 kB
Active:          57252 kB
Inactive:       113352 kB
HighTotal:      131008 kB
HighFree:        14448 kB
LowTotal:       903652 kB
LowFree:        825776 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18284 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:49:29 (client local time) WITH STATUS 30 IN 1115.3 SECONDS
stats: 16794 0 1115.3 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 115 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 113]---> Adder-cost: 273   maxlim: 13440   bits: 15/14
c ---[ 111]---> BDD-cost:   40
c ---[ 109]---> BDD-cost:   25
c ---[ 107]---> BDD-cost:   45
c ---[ 105]---> BDD-cost:   83
c ---[ 101]---> BDD-cost:   39
c ---[  99]---> BDD-cost:  100
c ---[  97]---> BDD-cost:   34
c ---[  91]---> BDD-cost:   55
c ---[  89]---> BDD-cost:   40
c ---[  85]---> BDD-cost:  128
c ---[  83]---> BDD-cost:   40
c ---[  81]---> BDD-cost:  112
c ---[  79]---> BDD-cost:   49
c ---[  75]---> BDD-cost:   45
c ---[  73]---> BDD-cost:   28
c ---[  71]---> Sorter-cost:  514     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> BDD-cost:   55
c ---[  67]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> BDD-cost:  118
c ---[  59]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   40
c ---[  55]---> BDD-cost:   40
c ---[  53]---> BDD-cost:   51
c ---[  49]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   49
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:   10
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   11
c ---[  37]---> BDD-cost:   12
c ---[  36]---> BDD-cost:   12
c ---[  35]---> BDD-cost:   12
c ---[  34]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   12
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   10
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   26
c ---[  17]---> BDD-cost:   26
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   26
c ---[  13]---> BDD-cost:   26
c ---[  12]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   26
c ---[   8]---> BDD-cost:   26
c ---[   7]---> BDD-cost:   26
c ---[   6]---> BDD-cost:   26
c ---[   4]---> BDD-cost:   26
c ---[   3]---> BDD-cost:   26
c ---[   2]---> BDD-cost:   26
c ---[   1]---> BDD-cost:   26
c ---[   0]---> BDD-cost:   26
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9294    24740 |    2788       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3125          
c   -- var.elim.:  2000/3125          
c   -- var.elim.:  3000/3125          
c   -- var.elim.:  3125/3125          
c   -- var.elim.:  1000/1652          
c   -- var.elim.:  1652/1652          
c   -- var.elim.:  71/71          
c   -- var.elim.:  34/34          
c   -- var.elim.:  43/43          
c   -- var.elim.:  50/50          
c   -- var.elim.:  44/44          
c   -- var.elim.:  37/37          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  545/545          
c   -- var.elim.:  501/501          
c   -- subsuming                       
c   -- var.elim.:  121/121          
c   -- var.elim.:  5/5          
c   -- var.elim.:  16/16          
c   -- var.elim.:  19/19          
c   -- var.elim.:  24/24          
c   -- var.elim.:  24/24          
c   -- var.elim.:  24/24          
c   -- var.elim.:  25/25          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  25/25          
c   -- var.elim.:  25/25          
c |         0 |    6801    20448 |      --       0       --      -- |     --   | -2046/-2783
c |         0 |    6801    20448 |    2720       0        0     nan |  0.000 % |
c |       100 |    6742    20182 |    2966      95      637     6.7 | 36.729 % |
c |       251 |    6517    19416 |    3154     229     1237     5.4 | 38.226 % |
c ==============================================================================
c (current CPU-time: 0.482926 s)
c ==============================================================================
c [1mFound solution: 94412024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:93452     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       345 |  270583   635896 |   81174     323     1978     6.1 | 38.226 % |
c   -- subsuming                       
c   -- var.elim.:  1000/89545          
c   -- var.elim.:  2000/89545          
c   -- var.elim.:  3000/89545          
c   -- var.elim.:  4000/89545          
c   -- var.elim.:  5000/89545          
c   -- var.elim.:  6000/89545          
c   -- var.elim.:  7000/89545          
c   -- var.elim.:  8000/89545          
c   -- var.elim.:  9000/89545          
c   -- var.elim.:  10000/89545          
c   -- var.elim.:  11000/89545          
c   -- var.elim.:  12000/89545          
c   -- var.elim.:  13000/89545          
c   -- var.elim.:  14000/89545          
c   -- var.elim.:  15000/89545          
c   -- var.elim.:  16000/89545          
c   -- var.elim.:  17000/89545          
c   -- var.elim.:  18000/89545          
c   -- var.elim.:  19000/89545          
c   -- var.elim.:  20000/89545          
c   -- var.elim.:  21000/89545          
c   -- var.elim.:  22000/89545          
c   -- var.elim.:  23000/89545          
c   -- var.elim.:  24000/89545          
c   -- var.elim.:  25000/89545          
c   -- var.elim.:  26000/89545          
c   -- var.elim.:  27000/89545          
c   -- var.elim.:  28000/89545          
c   -- var.elim.:  29000/89545          
c   -- var.elim.:  30000/89545          
c   -- var.elim.:  31000/89545          
c   -- var.elim.:  32000/89545          
c   -- var.elim.:  33000/89545          
c   -- var.elim.:  34000/89545          
c   -- var.elim.:  35000/89545          
c   -- var.elim.:  36000/89545          
c   -- var.elim.:  37000/89545          
c   -- var.elim.:  38000/89545          
c   -- var.elim.:  39000/89545          
c   -- var.elim.:  40000/89545          
c   -- var.elim.:  41000/89545          
c   -- var.elim.:  42000/89545          
c   -- var.elim.:  43000/89545          
c   -- var.elim.:  44000/89545          
c   -- var.elim.:  45000/89545          
c   -- var.elim.:  46000/89545          
c   -- var.elim.:  47000/89545          
c   -- var.elim.:  48000/89545          
c   -- var.elim.:  49000/89545          
c   -- var.elim.:  50000/89545          
c   -- var.elim.:  51000/89545          
c   -- var.elim.:  52000/89545          
c   -- var.elim.:  53000/89545          
c   -- var.elim.:  54000/89545          
c   -- var.elim.:  55000/89545          
c   -- var.elim.:  56000/89545          
c   -- var.elim.:  57000/89545          
c   -- var.elim.:  58000/89545          
c   -- var.elim.:  59000/89545          
c   -- var.elim.:  60000/89545          
c   -- var.elim.:  61000/89545          
c   -- var.elim.:  62000/89545          
c   -- var.elim.:  63000/89545          
c   -- var.elim.:  64000/89545          
c   -- var.elim.:  65000/89545          
c   -- var.elim.:  66000/89545          
c   -- var.elim.:  67000/89545          
c   -- var.elim.:  68000/89545          
c   -- var.elim.:  69000/89545          
c   -- var.elim.:  70000/89545          
c   -- var.elim.:  71000/89545          
c   -- var.elim.:  72000/89545          
c   -- var.elim.:  73000/89545          
c   -- var.elim.:  74000/89545          
c   -- var.elim.:  75000/89545          
c   -- var.elim.:  76000/89545          
c   -- var.elim.:  77000/89545          
c   -- var.elim.:  78000/89545          
c   -- var.elim.:  79000/89545          
c   -- var.elim.:  80000/89545          
c   -- var.elim.:  81000/89545          
c   -- var.elim.:  82000/89545          
c   -- var.elim.:  83000/89545          
c   -- var.elim.:  84000/89545          
c   -- var.elim.:  85000/89545          
c   -- var.elim.:  86000/89545          
c   -- var.elim.:  87000/89545          
c   -- var.elim.:  88000/89545          
c   -- var.elim.:  89000/89545          
c   -- var.elim.:  89545/89545          
c   -- var.elim.:  1000/49758          
c   -- var.elim.:  2000/49758          
c   -- var.elim.:  3000/49758          
c   -- var.elim.:  4000/49758          
c   -- var.elim.:  5000/49758          
c   -- var.elim.:  6000/49758          
c   -- var.elim.:  7000/49758          
c   -- var.elim.:  8000/49758          
c   -- var.elim.:  9000/49758          
c   -- var.elim.:  10000/49758          
c   -- var.elim.:  11000/49758          
c   -- var.elim.:  12000/49758          
c   -- var.elim.:  13000/49758          
c   -- var.elim.:  14000/49758          
c   -- var.elim.:  15000/49758          
c   -- var.elim.:  16000/49758          
c   -- var.elim.:  17000/49758          
c   -- var.elim.:  18000/49758          
c   -- var.elim.:  19000/49758          
c   -- var.elim.:  20000/49758          
c   -- var.elim.:  21000/49758          
c   -- var.elim.:  22000/49758          
c   -- var.elim.:  23000/49758          
c   -- var.elim.:  24000/49758          
c   -- var.elim.:  25000/49758          
c   -- var.elim.:  26000/49758          
c   -- var.elim.:  27000/49758          
c   -- var.elim.:  28000/49758          
c   -- var.elim.:  29000/49758          
c   -- var.elim.:  30000/49758          
c   -- var.elim.:  31000/49758          
c   -- var.elim.:  32000/49758          
c   -- var.elim.:  33000/49758          
c   -- var.elim.:  34000/49758          
c   -- var.elim.:  35000/49758          
c   -- var.elim.:  36000/49758          
c   -- var.elim.:  37000/49758          
c   -- var.elim.:  38000/49758          
c   -- var.elim.:  39000/49758          
c   -- var.elim.:  40000/49758          
c   -- var.elim.:  41000/49758          
c   -- var.elim.:  42000/49758          
c   -- var.elim.:  43000/49758          
c   -- var.elim.:  44000/49758          
c   -- var.elim.:  45000/49758          
c   -- var.elim.:  46000/49758          
c   -- var.elim.:  47000/49758          
c   -- var.elim.:  48000/49758          
c   -- var.elim.:  49000/49758          
c   -- var.elim.:  49758/49758          
c   -- var.elim.:  127/127          
c   -- var.elim.:  75/75          
c   -- var.elim.:  6/6          
c   -- subsuming                       
c   -- var.elim.:  1000/1446          
c   -- var.elim.:  1446/1446          
c   -- var.elim.:  468/468          
c   -- subsuming                       
c   -- var.elim.:  256/256          
c   -- var.elim.:  29/29          
c |       345 |  248090   757444 |      --     323       --      -- |     --   | -22493/121549
c |       345 |  248090   757444 |   99236     301     1800     6.0 | 38.226 % |
c |       445 |  248084   757387 |  109156     397     2220     5.6 |  2.080 % |
c |       595 |  248084   757387 |  120072     547     3379     6.2 |  2.080 % |
c |       820 |  248084   757387 |  132079     772    57833    74.9 |  2.080 % |
c ==============================================================================
c (current CPU-time: 19.0611 s)
c ==============================================================================
c [1mFound solution: 70732304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:54680     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       869 |  399177  1105754 |  119753     814    58560    71.9 |  2.080 % |
c   -- subsuming                       
c   -- var.elim.:  1000/56944          
c   -- var.elim.:  2000/56944          
c   -- var.elim.:  3000/56944          
c   -- var.elim.:  4000/56944          
c   -- var.elim.:  5000/56944          
c   -- var.elim.:  6000/56944          
c   -- var.elim.:  7000/56944          
c   -- var.elim.:  8000/56944          
c   -- var.elim.:  9000/56944          
c   -- var.elim.:  10000/56944          
c   -- var.elim.:  11000/56944          
c   -- var.elim.:  12000/56944          
c   -- var.elim.:  13000/56944          
c   -- var.elim.:  14000/56944          
c   -- var.elim.:  15000/56944          
c   -- var.elim.:  16000/56944          
c   -- var.elim.:  17000/56944          
c   -- var.elim.:  18000/56944          
c   -- var.elim.:  19000/56944          
c   -- var.elim.:  20000/56944          
c   -- var.elim.:  21000/56944          
c   -- var.elim.:  22000/56944          
c   -- var.elim.:  23000/56944          
c   -- var.elim.:  24000/56944          
c   -- var.elim.:  25000/56944          
c   -- var.elim.:  26000/56944          
c   -- var.elim.:  27000/56944          
c   -- var.elim.:  28000/56944          
c   -- var.elim.:  29000/56944          
c   -- var.elim.:  30000/56944          
c   -- var.elim.:  31000/56944          
c   -- var.elim.:  32000/56944          
c   -- var.elim.:  33000/56944          
c   -- var.elim.:  34000/56944          
c   -- var.elim.:  35000/56944          
c   -- var.elim.:  36000/56944          
c   -- var.elim.:  37000/56944          
c   -- var.elim.:  38000/56944          
c   -- var.elim.:  39000/56944          
c   -- var.elim.:  40000/56944          
c   -- var.elim.:  41000/56944          
c   -- var.elim.:  42000/56944          
c   -- var.elim.:  43000/56944          
c   -- var.elim.:  44000/56944          
c   -- var.elim.:  45000/56944          
c   -- var.elim.:  46000/56944          
c   -- var.elim.:  47000/56944          
c   -- var.elim.:  48000/56944          
c   -- var.elim.:  49000/56944          
c   -- var.elim.:  50000/56944          
c   -- var.elim.:  51000/56944          
c   -- var.elim.:  52000/56944          
c   -- var.elim.:  53000/56944          
c   -- var.elim.:  54000/56944          
c   -- var.elim.:  55000/56944          
c   -- var.elim.:  56000/56944          
c   -- var.elim.:  56944/56944          
c   -- var.elim.:  1000/31294          
c   -- var.elim.:  2000/31294          
c   -- var.elim.:  3000/31294          
c   -- var.elim.:  4000/31294          
c   -- var.elim.:  5000/31294          
c   -- var.elim.:  6000/31294          
c   -- var.elim.:  7000/31294          
c   -- var.elim.:  8000/31294          
c   -- var.elim.:  9000/31294          
c   -- var.elim.:  10000/31294          
c   -- var.elim.:  11000/31294          
c   -- var.elim.:  12000/31294          
c   -- var.elim.:  13000/31294          
c   -- var.elim.:  14000/31294          
c   -- var.elim.:  15000/31294          
c   -- var.elim.:  16000/31294          
c   -- var.elim.:  17000/31294          
c   -- var.elim.:  18000/31294          
c   -- var.elim.:  19000/31294          
c   -- var.elim.:  20000/31294          
c   -- var.elim.:  21000/31294          
c   -- var.elim.:  22000/31294          
c   -- var.elim.:  23000/31294          
c   -- var.elim.:  24000/31294          
c   -- var.elim.:  25000/31294          
c   -- var.elim.:  26000/31294          
c   -- var.elim.:  27000/31294          
c   -- var.elim.:  28000/31294          
c   -- var.elim.:  29000/31294          
c   -- var.elim.:  30000/31294          
c   -- var.elim.:  31000/31294          
c   -- var.elim.:  31294/31294          
c   -- var.elim.:  49/49          
c   -- subsuming                       
c   -- var.elim.:  1000/1350          
c   -- var.elim.:  1350/1350          
c   -- var.elim.:  215/215          
c   -- subsuming                       
c   -- var.elim.:  279/279          
c   -- var.elim.:  69/69          
c |       869 |  384499  1177781 |      --     814       --      -- |     --   | -14658/72073
c |       869 |  384499  1177781 |  153799     785    29753    37.9 |  2.080 % |
c |       970 |  383777  1173591 |  168861     882    30671    34.8 |  1.987 % |
c |      1120 |  381536  1165586 |  184663    1030    31778    30.9 |  2.372 % |
c |      1345 |  376315  1147127 |  200350    1237    34570    27.9 |  3.382 % |
c |      1684 |  374464  1141109 |  219301    1565    37272    23.8 |  3.780 % |
c |      2192 |  371954  1131568 |  239614    2045    58424    28.6 |  4.236 % |
c ==============================================================================
c (current CPU-time: 44.3343 s)
c ==============================================================================
c [1mFound solution: 70467328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:53250     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2590 |  521401  1480993 |  156420    2441    77032    31.6 |  4.236 % |
c   -- subsuming                       
c   -- var.elim.:  1000/61134          
c   -- var.elim.:  2000/61134          
c   -- var.elim.:  3000/61134          
c   -- var.elim.:  4000/61134          
c   -- var.elim.:  5000/61134          
c   -- var.elim.:  6000/61134          
c   -- var.elim.:  7000/61134          
c   -- var.elim.:  8000/61134          
c   -- var.elim.:  9000/61134          
c   -- var.elim.:  10000/61134          
c   -- var.elim.:  11000/61134          
c   -- var.elim.:  12000/61134          
c   -- var.elim.:  13000/61134          
c   -- var.elim.:  14000/61134          
c   -- var.elim.:  15000/61134          
c   -- var.elim.:  16000/61134          
c   -- var.elim.:  17000/61134          
c   -- var.elim.:  18000/61134          
c   -- var.elim.:  19000/61134          
c   -- var.elim.:  20000/61134          
c   -- var.elim.:  21000/61134          
c   -- var.elim.:  22000/61134          
c   -- var.elim.:  23000/61134          
c   -- var.elim.:  24000/61134          
c   -- var.elim.:  25000/61134          
c   -- var.elim.:  26000/61134          
c   -- var.elim.:  27000/61134          
c   -- var.elim.:  28000/61134          
c   -- var.elim.:  29000/61134          
c   -- var.elim.:  30000/61134          
c   -- var.elim.:  31000/61134          
c   -- var.elim.:  32000/61134          
c   -- var.elim.:  33000/61134          
c   -- var.elim.:  34000/61134          
c   -- var.elim.:  35000/61134          
c   -- var.elim.:  36000/61134          
c   -- var.elim.:  37000/61134          
c   -- var.elim.:  38000/61134          
c   -- var.elim.:  39000/61134          
c   -- var.elim.:  40000/61134          
c   -- var.elim.:  41000/61134          
c   -- var.elim.:  42000/61134          
c   -- var.elim.:  43000/61134          
c   -- var.elim.:  44000/61134          
c   -- var.elim.:  45000/61134          
c   -- var.elim.:  46000/61134          
c   -- var.elim.:  47000/61134          
c   -- var.elim.:  48000/61134          
c   -- var.elim.:  49000/61134          
c   -- var.elim.:  50000/61134          
c   -- var.elim.:  51000/61134          
c   -- var.elim.:  52000/61134          
c   -- var.elim.:  53000/61134          
c   -- var.elim.:  54000/61134          
c   -- var.elim.:  55000/61134          
c   -- var.elim.:  56000/61134          
c   -- var.elim.:  57000/61134          
c   -- var.elim.:  58000/61134          
c   -- var.elim.:  59000/61134          
c   -- var.elim.:  60000/61134          
c   -- var.elim.:  61000/61134          
c   -- var.elim.:  61134/61134          
c   -- var.elim.:  1000/33752          
c   -- var.elim.:  2000/33752          
c   -- var.elim.:  3000/33752          
c   -- var.elim.:  4000/33752          
c   -- var.elim.:  5000/33752          
c   -- var.elim.:  6000/33752          
c   -- var.elim.:  7000/33752          
c   -- var.elim.:  8000/33752          
c   -- var.elim.:  9000/33752          
c   -- var.elim.:  10000/33752          
c   -- var.elim.:  11000/33752          
c   -- var.elim.:  12000/33752          
c   -- var.elim.:  13000/33752          
c   -- var.elim.:  14000/33752          
c   -- var.elim.:  15000/33752          
c   -- var.elim.:  16000/33752          
c   -- var.elim.:  17000/33752          
c   -- var.elim.:  18000/33752          
c   -- var.elim.:  19000/33752          
c   -- var.elim.:  20000/33752          
c   -- var.elim.:  21000/33752          
c   -- var.elim.:  22000/33752          
c   -- var.elim.:  23000/33752          
c   -- var.elim.:  24000/33752          
c   -- var.elim.:  25000/33752          
c   -- var.elim.:  26000/33752          
c   -- var.elim.:  27000/33752          
c   -- var.elim.:  28000/33752          
c   -- var.elim.:  29000/33752          
c   -- var.elim.:  30000/33752          
c   -- var.elim.:  31000/33752          
c   -- var.elim.:  32000/33752          
c   -- var.elim.:  33000/33752          
c   -- var.elim.:  33752/33752          
c   -- var.elim.:  1000/1598          
c   -- var.elim.:  1598/1598          
c   -- var.elim.:  1000/1019          
c   -- var.elim.:  1019/1019          
c   -- var.elim.:  304/304          
c   -- var.elim.:  168/168          
c   -- subsuming                       
c   -- var.elim.:  1000/1339          
c   -- var.elim.:  1339/1339          
c   -- var.elim.:  662/662          
c   -- subsuming                       
c   -- var.elim.:  544/544          
c   -- var.elim.:  30/30          
c |      2590 |  505864  1551351 |      --    2441       --      -- |     --   | -15355/70784
c |      2590 |  505864  1551351 |  202345    2030    21031    10.4 |  4.236 % |
c ==============================================================================
c (current CPU-time: 58.1022 s)
c ==============================================================================
c [1mFound solution: 70067968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2603 |  505994  1551979 |  151798    2043    23375    11.4 |  4.236 % |
c   -- subsuming                       
c   -- var.elim.:  515/515          
c   -- var.elim.:  411/411          
c   -- var.elim.:  8/8          
c |      2603 |  505915  1552502 |      --    2043       --      -- |     --   | -79/524
c |      2603 |  505915  1552502 |  202366    2043    23375    11.4 |  4.236 % |
c |      2703 |  505769  1552016 |  222538    2141    24980    11.7 |  3.369 % |
c |      2854 |  505653  1551628 |  244736    2290    26935    11.8 |  3.385 % |
c |      3079 |  505426  1550684 |  269088    2513    46001    18.3 |  3.406 % |
c |      3416 |  505426  1550684 |  295997    2850   115742    40.6 |  3.406 % |
c |      3922 |  505426  1550684 |  325597    3356   153233    45.7 |  3.406 % |
c ==============================================================================
c (current CPU-time: 91.5831 s)
c ==============================================================================
c [1mFound solution: 67903160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4062 |  507766  1556719 |  152329    3495   163846    46.9 |  3.406 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5068          
c   -- var.elim.:  2000/5068          
c   -- var.elim.:  3000/5068          
c   -- var.elim.:  4000/5068          
c   -- var.elim.:  5000/5068          
c   -- var.elim.:  5068/5068          
c   -- var.elim.:  1000/2786          
c   -- var.elim.:  2000/2786          
c   -- var.elim.:  2786/2786          
c   -- var.elim.:  155/155          
c   -- subsuming                       
c   -- var.elim.:  38/38          
c   -- var.elim.:  27/27          
c |      4062 |  506341  1557635 |      --    3495       --      -- |     --   | -1424/919
c |      4062 |  506341  1557635 |  202536    3372   126958    37.7 |  3.406 % |
c ==============================================================================
c (current CPU-time: 99.3729 s)
c ==============================================================================
c [1mFound solution: 66462810[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4146 |  507116  1560366 |  152134    3454   136915    39.6 |  3.406 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3016          
c   -- var.elim.:  2000/3016          
c   -- var.elim.:  3000/3016          
c   -- var.elim.:  3016/3016          
c   -- var.elim.:  1000/2083          
c   -- var.elim.:  2000/2083          
c   -- var.elim.:  2083/2083          
c   -- var.elim.:  278/278          
c   -- var.elim.:  46/46          
c   -- subsuming                       
c   -- var.elim.:  148/148          
c   -- var.elim.:  139/139          
c |      4146 |  506436  1562078 |      --    3454       --      -- |     --   | -680/1713
c |      4146 |  506436  1562078 |  202574    3443   129888    37.7 |  3.406 % |
c |      4246 |  506436  1562078 |  222831    3543   140087    39.5 |  3.460 % |
c |      4396 |  506436  1562078 |  245115    3693   146252    39.6 |  3.460 % |
c |      4621 |  506436  1562078 |  269626    3918   242466    61.9 |  3.460 % |
c |      4958 |  506436  1562078 |  296589    4255   267265    62.8 |  3.460 % |
c |      5464 |  506046  1559611 |  325996    4758   358670    75.4 |  3.508 % |
c |      6223 |  505973  1559373 |  358544    5510   507800    92.2 |  3.520 % |
c ==============================================================================
c (current CPU-time: 157.425 s)
c ==============================================================================
c [1mFound solution: 66461504[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6486 |  506113  1560886 |  151833    5773   589969   102.2 |  3.520 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2072          
c   -- var.elim.:  2000/2072          
c   -- var.elim.:  2072/2072          
c   -- var.elim.:  1000/1525          
c   -- var.elim.:  1525/1525          
c   -- var.elim.:  455/455          
c   -- subsuming                       
c   -- var.elim.:  158/158          
c   -- var.elim.:  143/143          
c |      6486 |  505952  1563004 |      --    5773       --      -- |     --   | -160/2121
c |      6486 |  505952  1563004 |  202380    5253   289643    55.1 |  3.520 % |
c |      6587 |  505908  1562552 |  222599    5353   297441    55.6 |  3.530 % |
c |      6738 |  505888  1562487 |  244849    5503   326600    59.3 |  3.532 % |
c |      6963 |  505888  1562487 |  269334    5728   333989    58.3 |  3.532 % |
c |      7300 |  505322  1560071 |  295936    6062   336170    55.5 |  3.591 % |
c |      7807 |  505060  1557373 |  325361    6564   339878    51.8 |  3.619 % |
c |      8567 |  505060  1557373 |  357897    7324   489399    66.8 |  3.619 % |
c |      9707 |  504906  1556827 |  393567    8457   903182   106.8 |  3.645 % |
c ==============================================================================
c (current CPU-time: 214.605 s)
c ==============================================================================
c [1mFound solution: 66454400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9884 |  504980  1558083 |  151493    8624   922339   107.0 |  3.645 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3567          
c   -- var.elim.:  2000/3567          
c   -- var.elim.:  3000/3567          
c   -- var.elim.:  3567/3567          
c   -- var.elim.:  1000/2517          
c   -- var.elim.:  2000/2517          
c   -- var.elim.:  2517/2517          
c   -- var.elim.:  729/729          
c   -- subsuming                       
c   -- var.elim.:  159/159          
c   -- var.elim.:  135/135          
c |      9884 |  504704  1560459 |      --    8624       --      -- |     --   | -275/2379
c |      9884 |  504704  1560459 |  201881    7420   310978    41.9 |  3.645 % |
c |      9984 |  504684  1560387 |  222060    7519   314657    41.8 |  3.669 % |
c |     10134 |  504684  1560387 |  244267    7669   316242    41.2 |  3.669 % |
c |     10361 |  504684  1560387 |  268693    7896   349549    44.3 |  3.669 % |
c |     10698 |  504684  1560387 |  295563    8233   391596    47.6 |  3.669 % |
c |     11206 |  504684  1560387 |  325119    8741   502813    57.5 |  3.669 % |
c ==============================================================================
c (current CPU-time: 259.386 s)
c ==============================================================================
c [1mFound solution: 66066068[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11776 |  505339  1563400 |  151601    9311   598755    64.3 |  3.669 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2311          
c   -- var.elim.:  2000/2311          
c   -- var.elim.:  2311/2311          
c   -- var.elim.:  1000/1736          
c   -- var.elim.:  1736/1736          
c   -- var.elim.:  898/898          
c   -- var.elim.:  767/767          
c   -- subsuming                       
c   -- var.elim.:  65/65          
c |     11776 |  504730  1563693 |      --    9311       --      -- |     --   | -609/294
c |     11776 |  504730  1563693 |  201892    9310   598705    64.3 |  3.669 % |
c |     11876 |  504730  1563693 |  222081    9410   599957    63.8 |  3.671 % |
c |     12026 |  504730  1563693 |  244289    9560   601135    62.9 |  3.671 % |
c |     12251 |  504578  1562275 |  268637    9783   615730    62.9 |  3.690 % |
c |     12588 |  504421  1561399 |  295409   10119   734103    72.5 |  3.707 % |
c |     13095 |  503459  1554636 |  324330   10604   865825    81.7 |  3.804 % |
c ==============================================================================
c (current CPU-time: 297.941 s)
c ==============================================================================
c [1mFound solution: 65826944[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:33758     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13648 |  596159  1770848 |  178847   11156  1007321    90.3 |  3.804 % |
c   -- subsuming                       
c   -- var.elim.:  1000/36509          
c   -- var.elim.:  2000/36509          
c   -- var.elim.:  3000/36509          
c   -- var.elim.:  4000/36509          
c   -- var.elim.:  5000/36509          
c   -- var.elim.:  6000/36509          
c   -- var.elim.:  7000/36509          
c   -- var.elim.:  8000/36509          
c   -- var.elim.:  9000/36509          
c   -- var.elim.:  10000/36509          
c   -- var.elim.:  11000/36509          
c   -- var.elim.:  12000/36509          
c   -- var.elim.:  13000/36509          
c   -- var.elim.:  14000/36509          
c   -- var.elim.:  15000/36509          
c   -- var.elim.:  16000/36509          
c   -- var.elim.:  17000/36509          
c   -- var.elim.:  18000/36509          
c   -- var.elim.:  19000/36509          
c   -- var.elim.:  20000/36509          
c   -- var.elim.:  21000/36509          
c   -- var.elim.:  22000/36509          
c   -- var.elim.:  23000/36509          
c   -- var.elim.:  24000/36509          
c   -- var.elim.:  25000/36509          
c   -- var.elim.:  26000/36509          
c   -- var.elim.:  27000/36509          
c   -- var.elim.:  28000/36509          
c   -- var.elim.:  29000/36509          
c   -- var.elim.:  30000/36509          
c   -- var.elim.:  31000/36509          
c   -- var.elim.:  32000/36509          
c   -- var.elim.:  33000/36509          
c   -- var.elim.:  34000/36509          
c   -- var.elim.:  35000/36509          
c   -- var.elim.:  36000/36509          
c   -- var.elim.:  36509/36509          
c   -- var.elim.:  1000/20680          
c   -- var.elim.:  2000/20680          
c   -- var.elim.:  3000/20680          
c   -- var.elim.:  4000/20680          
c   -- var.elim.:  5000/20680          
c   -- var.elim.:  6000/20680          
c   -- var.elim.:  7000/20680          
c   -- var.elim.:  8000/20680          
c   -- var.elim.:  9000/20680          
c   -- var.elim.:  10000/20680          
c   -- var.elim.:  11000/20680          
c   -- var.elim.:  12000/20680          
c   -- var.elim.:  13000/20680          
c   -- var.elim.:  14000/20680          
c   -- var.elim.:  15000/20680          
c   -- var.elim.:  16000/20680          
c   -- var.elim.:  17000/20680          
c   -- var.elim.:  18000/20680          
c   -- var.elim.:  19000/20680          
c   -- var.elim.:  20000/20680          
c   -- var.elim.:  20680/20680          
c   -- var.elim.:  1000/1524          
c   -- var.elim.:  1524/1524          
c   -- var.elim.:  528/528          
c   -- subsuming                       
c   -- var.elim.:  1000/1440          
c   -- var.elim.:  1440/1440          
c   -- var.elim.:  1000/1664          
c   -- var.elim.:  1664/1664          
c   -- var.elim.:  1000/1094          
c   -- var.elim.:  1094/1094          
c   -- subsuming                       
c   -- var.elim.:  93/93          
c   -- var.elim.:  9/9          
c |     13648 |  585452  1812114 |      --   11156       --      -- |     --   | -10338/42121
c |     13648 |  585452  1812114 |  234180   10283   429024    41.7 |  3.804 % |
c |     13748 |  585452  1812114 |  257598   10383   441529    42.5 |  3.594 % |
c |     13899 |  585452  1812114 |  283358   10534   489244    46.4 |  3.594 % |
c |     14124 |  585452  1812114 |  311694   10759   496754    46.2 |  3.594 % |
c ==============================================================================
c (current CPU-time: 324.674 s)
c ==============================================================================
c [1mFound solution: 65062528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14416 |  586810  1816196 |  176042   11046   541094    49.0 |  3.594 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2837          
c   -- var.elim.:  2000/2837          
c   -- var.elim.:  2837/2837          
c   -- var.elim.:  1000/1769          
c   -- var.elim.:  1769/1769          
c   -- var.elim.:  515/515          
c   -- subsuming                       
c   -- var.elim.:  199/199          
c   -- var.elim.:  131/131          
c |     14416 |  585969  1817622 |      --   11046       --      -- |     --   | -836/1437
c |     14416 |  585969  1817622 |  234387   10339   417242    40.4 |  3.594 % |
c |     14516 |  585969  1817622 |  257826   10439   437664    41.9 |  3.603 % |
c |     14667 |  585969  1817622 |  283608   10590   446249    42.1 |  3.603 % |
c |     14892 |  585688  1816192 |  311820   10811   496441    45.9 |  3.640 % |
c ==============================================================================
c (current CPU-time: 350.331 s)
c ==============================================================================
c [1mFound solution: 65052960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15053 |  587056  1820806 |  176116   10972   580851    52.9 |  3.640 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3385          
c   -- var.elim.:  2000/3385          
c   -- var.elim.:  3000/3385          
c   -- var.elim.:  3385/3385          
c   -- var.elim.:  1000/2271          
c   -- var.elim.:  2000/2271          
c   -- var.elim.:  2271/2271          
c   -- var.elim.:  392/392          
c   -- var.elim.:  1000/1123          
c   -- var.elim.:  1123/1123          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c |     15053 |  586193  1826238 |      --   10972       --      -- |     --   | -861/5437
c |     15053 |  586193  1826238 |  234477   10881   537150    49.4 |  3.640 % |
c |     15153 |  586193  1826238 |  257924   10981   538312    49.0 |  3.643 % |
c |     15303 |  585688  1823059 |  283472   11129   539399    48.5 |  3.685 % |
c |     15529 |  585688  1823059 |  311820   11355   622884    54.9 |  3.685 % |
c |     15867 |  585688  1823059 |  343002   11693   742449    63.5 |  3.685 % |
c |     16374 |  585590  1822695 |  377239   12192   889509    73.0 |  3.696 % |
c ==============================================================================
c (current CPU-time: 396.642 s)
c ==============================================================================
c [1mFound solution: 64891520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     16495 |  586891  1826784 |  176067   12313   963726    78.3 |  3.696 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3896          
c   -- var.elim.:  2000/3896          
c   -- var.elim.:  3000/3896          
c   -- var.elim.:  3896/3896          
c   -- var.elim.:  1000/2539          
c   -- var.elim.:  2000/2539          
c   -- var.elim.:  2539/2539          
c   -- var.elim.:  648/648          
c   -- var.elim.:  221/221          
c   -- subsuming                       
c   -- var.elim.:  279/279          
c   -- var.elim.:  8/8          
c |     16495 |  585986  1829322 |      --   12313       --      -- |     --   | -903/2543
c |     16495 |  585986  1829322 |  234394   11812   489711    41.5 |  3.696 % |
c |     16595 |  585966  1829254 |  257825   11911   493286    41.4 |  3.702 % |
c |     16745 |  585732  1827217 |  283494   12059   494394    41.0 |  3.726 % |
c |     16971 |  585639  1826624 |  311794   12280   503790    41.0 |  3.735 % |
c |     17309 |  585434  1825746 |  342853   12616   576486    45.7 |  3.753 % |
c |     17815 |  585434  1825746 |  377138   13122   804322    61.3 |  3.753 % |
c ==============================================================================
c (current CPU-time: 437.252 s)
c ==============================================================================
c [1mFound solution: 64890112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17931 |  585598  1827307 |  175679   13238   838559    63.3 |  3.753 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2160          
c   -- var.elim.:  2000/2160          
c   -- var.elim.:  2160/2160          
c   -- var.elim.:  1000/1699          
c   -- var.elim.:  1699/1699          
c   -- var.elim.:  378/378          
c   -- var.elim.:  1/1          
c   -- subsuming                       
c |     17931 |  585422  1831015 |      --   13238       --      -- |     --   | -173/3715
c |     17931 |  585422  1831015 |  234168   13143   795395    60.5 |  3.753 % |
c ==============================================================================
c (current CPU-time: 442.277 s)
c ==============================================================================
c [1mFound solution: 62902528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17943 |  585565  1832562 |  175669   13155   796265    60.5 |  3.753 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1382          
c   -- var.elim.:  1382/1382          
c   -- var.elim.:  1000/1304          
c   -- var.elim.:  1304/1304          
c   -- var.elim.:  440/440          
c   -- var.elim.:  124/124          
c |     17943 |  585460  1834848 |      --   13155       --      -- |     --   | -105/2287
c |     17943 |  585460  1834848 |  234184   13155   796265    60.5 |  3.753 % |
c |     18043 |  585460  1834848 |  257602   13255   807922    61.0 |  3.757 % |
c |     18193 |  585460  1834848 |  283362   13405   812642    60.6 |  3.757 % |
c |     18418 |  585460  1834848 |  311698   13630   872055    64.0 |  3.757 % |
c |     18757 |  585327  1834265 |  342790   13967   946994    67.8 |  3.773 % |
c |     19263 |  585327  1834265 |  377069   14473  1034627    71.5 |  3.773 % |
c ==============================================================================
c (current CPU-time: 491.722 s)
c ==============================================================================
c [1mFound solution: 62498816[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19350 |  585459  1835737 |  175637   14560  1053465    72.4 |  3.773 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1645          
c   -- var.elim.:  1645/1645          
c   -- var.elim.:  1000/1302          
c   -- var.elim.:  1302/1302          
c   -- var.elim.:  976/976          
c   -- var.elim.:  258/258          
c   -- subsuming                       
c   -- var.elim.:  223/223          
c   -- var.elim.:  9/9          
c |     19350 |  585347  1837773 |      --   14560       --      -- |     --   | -112/2037
c |     19350 |  585347  1837773 |  234138   14422   900111    62.4 |  3.773 % |
c |     19452 |  585347  1837773 |  257552   14524   923278    63.6 |  3.774 % |
c |     19602 |  585159  1836946 |  283216   14629   945990    64.7 |  3.796 % |
c |     19828 |  585159  1836946 |  311538   14855  1041763    70.1 |  3.796 % |
c |     20170 |  585096  1836733 |  342655   15189  1205003    79.3 |  3.806 % |
c ==============================================================================
c (current CPU-time: 526.967 s)
c ==============================================================================
c [1mFound solution: 60044288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20270 |  585233  1838141 |  175569   15289  1223779    80.0 |  3.806 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1731          
c   -- var.elim.:  1731/1731          
c   -- var.elim.:  1000/1322          
c   -- var.elim.:  1322/1322          
c   -- var.elim.:  962/962          
c   -- subsuming                       
c   -- var.elim.:  239/239          
c   -- var.elim.:  11/11          
c |     20270 |  585126  1840394 |      --   15289       --      -- |     --   | -107/2254
c |     20270 |  585126  1840394 |  234050   14059   653803    46.5 |  3.806 % |
c |     20370 |  585126  1840394 |  257455   14159   657181    46.4 |  3.807 % |
c |     20520 |  585088  1840212 |  283182   14307   688852    48.1 |  3.817 % |
c |     20745 |  584427  1831300 |  311148   14529   712511    49.0 |  3.879 % |
c ==============================================================================
c (current CPU-time: 552.157 s)
c ==============================================================================
c [1mFound solution: 59517056[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20901 |  584513  1831985 |  175353   14685   739277    50.3 |  3.879 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1654          
c   -- var.elim.:  1654/1654          
c   -- var.elim.:  1000/1758          
c   -- var.elim.:  1758/1758          
c   -- var.elim.:  142/142          
c   -- subsuming                       
c   -- var.elim.:  319/319          
c |     20901 |  584390  1835716 |      --   14685       --      -- |     --   | -120/3738
c |     20901 |  584390  1835716 |  233756   13819   556953    40.3 |  3.879 % |
c |     21002 |  584390  1835716 |  257131   13920   577074    41.5 |  3.884 % |
c |     21152 |  584390  1835716 |  282844   14070   633550    45.0 |  3.884 % |
c |     21378 |  584390  1835716 |  311129   14296   679919    47.6 |  3.884 % |
c |     21715 |  584390  1835716 |  342242   14633   763479    52.2 |  3.884 % |
c |     22221 |  584390  1835716 |  376466   15139   922880    61.0 |  3.884 % |
c |     22981 |  584390  1835716 |  414113   15899  1232446    77.5 |  3.884 % |
c ==============================================================================
c (current CPU-time: 643.319 s)
c ==============================================================================
c [1mFound solution: 59075456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23485 |  584528  1837027 |  175358   16403  1411697    86.1 |  3.884 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1158          
c   -- var.elim.:  1158/1158          
c   -- var.elim.:  1000/1075          
c   -- var.elim.:  1075/1075          
c   -- var.elim.:  735/735          
c   -- var.elim.:  244/244          
c |     23485 |  584416  1838187 |      --   16403       --      -- |     --   | -111/1163
c |     23485 |  584416  1838187 |  233766   16403  1411697    86.1 |  3.884 % |
c |     23585 |  584416  1838187 |  257143   16503  1451516    88.0 |  3.885 % |
c |     23736 |  584416  1838187 |  282857   16654  1473611    88.5 |  3.885 % |
c |     23963 |  584416  1838187 |  311143   16881  1541237    91.3 |  3.885 % |
c |     24301 |  584416  1838187 |  342257   17219  1677604    97.4 |  3.885 % |
c |     24808 |  584416  1838187 |  376483   17726  1831756   103.3 |  3.885 % |
c |     25567 |  584416  1838187 |  414131   18485  2177947   117.8 |  3.885 % |
c |     26706 |  584416  1838187 |  455544   19624  2620886   133.6 |  3.885 % |
c ==============================================================================
c (current CPU-time: 791.01 s)
c ==============================================================================
c [1mFound solution: 58880896[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     27812 |  584502  1839181 |  175350   20730  3432073   165.6 |  3.885 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1022          
c   -- var.elim.:  1022/1022          
c   -- var.elim.:  850/850          
c   -- var.elim.:  767/767          
c   -- var.elim.:  746/746          
c |     27812 |  584434  1842017 |      --   20730       --      -- |     --   | -68/2837
c |     27812 |  584434  1842017 |  233773   20730  3432073   165.6 |  3.885 % |
c |     27912 |  584434  1842017 |  257150   20830  3453721   165.8 |  3.886 % |
c |     28064 |  584434  1842017 |  282866   20982  3507109   167.1 |  3.886 % |
c |     28290 |  584419  1841925 |  311144   21160  3706143   175.1 |  3.888 % |
c |     28628 |  584419  1841925 |  342259   21498  3891540   181.0 |  3.888 % |
c |     29134 |  584419  1841925 |  376485   22004  4270291   194.1 |  3.888 % |
c |     29893 |  584287  1840142 |  414040   22758  4441975   195.2 |  3.908 % |
c |     31034 |  583999  1839099 |  455219   23634  5078565   214.9 |  3.945 % |
c |     32743 |  582536  1832162 |  499487   19649  1915348    97.5 |  4.098 % |
c |     35307 |  582497  1832028 |  549398   22207  3053647   137.5 |  4.102 % |
c ==============================================================================
c [1mOptimal solution: 58880896[0m
s OPTIMUM FOUND
v I_0x2e_001_0x2e__0x2e__0x2e__bit0 -I_0x2e_001003_bit0 -I_0x2e_002003_bit0 -I_0x2e_002_0x2e__0x2e__0x2e__bit0 -I_0x2e_003005_bit0 I_0x2e_004005_bit0 -I_0x2e_004_0x2e__0x2e__0x2e__bit0 I_0x2e_005007_bit0 I_0x2e_006007_bit0 I_0x2e_007008_bit0 I_0x2e_008_0x2e__0x2e__0x2e__bit0 -I_0x2e_008009_bit0 I_0x2e_010012_bit0 I_0x2e_011012_bit0 -I_0x2e_012_0x2e__0x2e__0x2e__bit0 I_0x2e_012013_bit0 I_0x2e_013016_bit0 -I_0x2e_014015_bit0 I_0x2e_015016_bit0 I_0x2e_016_0x2e__0x2e__0x2e__bit0 -I_0x2e_016017_bit0 -I_0x2e_017018_bit0 -I_0x2e_009018_bit0 -I_0x2e_018019_bit0 I_0x2e_019024_bit0 -I_0x2e_024_0x2e__0x2e__0x2e__bit0 -I_0x2e_023024_bit0 -I_0x2e_022023_bit0 -I_0x2e_020022_bit0 I_0x2e_021022_bit0 I_0x2e_022_0x2e__0x2e__0x2e__bit0 I_0x2e_024026_bit0 I_0x2e_025026_bit0 -I_0x2e_025_0x2e__0x2e__0x2e__bit0 I_0x2e_026027_bit0 -I_0x2e_027_0x2e__0x2e__0x2e__bit0 I_0x2e_027032_bit0 -I_0x2e_030031_bit0 I_0x2e_031032_bit0 I_0x2e_029031_bit0 -I_0x2e_028029_bit0 -I_0x2e_028_0x2e__0x2e__0x2e__bit0 I_0x2e_032033_bit0 I_0x2e_033037_bit0 -I_0x2e_036037_bit0 -I_0x2e_034036_bit0 -I_0x2e_035036_bit0 I_0x2e_037038_bit0 I_0x2e_038040_bit0 I_0x2e_039040_bit0 -I_0x2e_040_0x2e__0x2e__0x2e__bit0 -I_0x2e_041_0x2e__0x2e__0x2e__bit0 I_0x2e_040041_bit0 I_0x2e_041042_bit0 I_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_001_0x2e__0x2e__0x2e__bit_7 -F_0x2e_001_0x2e__0x2e__0x2e__bit_6 -F_0x2e_001_0x2e__0x2e__0x2e__bit_5 -F_0x2e_001_0x2e__0x2e__0x2e__bit_4 -F_0x2e_001_0x2e__0x2e__0x2e__bit_3 -F_0x2e_001_0x2e__0x2e__0x2e__bit_2 -F_0x2e_001_0x2e__0x2e__0x2e__bit_1 -F_0x2e_001_0x2e__0x2e__0x2e__bit0 F_0x2e_001_0x2e__0x2e__0x2e__bit1 -F_0x2e_001_0x2e__0x2e__0x2e__bit2 -F_0x2e_001_0x2e__0x2e__0x2e__bit3 -F_0x2e_001_0x2e__0x2e__0x2e__bit4 -F_0x2e_001_0x2e__0x2e__0x2e__bit5 -F_0x2e_001_0x2e__0x2e__0x2e__bit6 -F_0x2e_001_0x2e__0x2e__0x2e__bit7 -F_0x2e_001_0x2e__0x2e__0x2e__bit8 -F_0x2e_001_0x2e__0x2e__0x2e__bit9 -F_0x2e_001_0x2e__0x2e__0x2e__bit10 -F_0x2e_001_0x2e__0x2e__0x2e__bit11 -F_0x2e_001_0x2e__0x2e__0x2e__bit12 -F_0x2e_001003_bit_7 -F_0x2e_001003_bit_6 -F_0x2e_001003_bit_5 -F_0x2e_001003_bit_4 -F_0x2e_001003_bit_3 -F_0x2e_001003_bit_2 -F_0x2e_001003_bit_1 -F_0x2e_001003_bit0 -F_0x2e_001003_bit1 -F_0x2e_001003_bit2 -F_0x2e_001003_bit3 -F_0x2e_001003_bit4 -F_0x2e_001003_bit5 -F_0x2e_001003_bit6 -F_0x2e_001003_bit7 -F_0x2e_001003_bit8 -F_0x2e_001003_bit9 -F_0x2e_001003_bit10 -F_0x2e_001003_bit11 -F_0x2e_001003_bit12 -F_0x2e_002003_bit_7 -F_0x2e_002003_bit_6 -F_0x2e_002003_bit_5 -F_0x2e_002003_bit_4 -F_0x2e_002003_bit_3 -F_0x2e_002003_bit_2 -F_0x2e_002003_bit_1 -F_0x2e_002003_bit0 -F_0x2e_002003_bit1 -F_0x2e_002003_bit2 -F_0x2e_002003_bit3 -F_0x2e_002003_bit4 -F_0x2e_002003_bit5 -F_0x2e_002003_bit6 -F_0x2e_002003_bit7 -F_0x2e_002003_bit8 -F_0x2e_002003_bit9 -F_0x2e_002003_bit10 -F_0x2e_002003_bit11 -F_0x2e_002003_bit12 -F_0x2e_002_0x2e__0x2e__0x2e__bit_7 -F_0x2e_002_0x2e__0x2e__0x2e__bit_6 -F_0x2e_002_0x2e__0x2e__0x2e__bit_5 -F_0x2e_002_0x2e__0x2e__0x2e__bit_4 -F_0x2e_002_0x2e__0x2e__0x2e__bit_3 -F_0x2e_002_0x2e__0x2e__0x2e__bit_2 -F_0x2e_002_0x2e__0x2e__0x2e__bit_1 -F_0x2e_002_0x2e__0x2e__0x2e__bit0 -F_0x2e_002_0x2e__0x2e__0x2e__bit1 -F_0x2e_002_0x2e__0x2e__0x2e__bit2 -F_0x2e_002_0x2e__0x2e__0x2e__bit3 -F_0x2e_002_0x2e__0x2e__0x2e__bit4 -F_0x2e_002_0x2e__0x2e__0x2e__bit5 -F_0x2e_002_0x2e__0x2e__0x2e__bit6 -F_0x2e_002_0x2e__0x2e__0x2e__bit7 -F_0x2e_002_0x2e__0x2e__0x2e__bit8 -F_0x2e_002_0x2e__0x2e__0x2e__bit9 -F_0x2e_002_0x2e__0x2e__0x2e__bit10 -F_0x2e_002_0x2e__0x2e__0x2e__bit11 -F_0x2e_002_0x2e__0x2e__0x2e__bit12 -F_0x2e_003005_bit_7 -F_0x2e_003005_bit_6 -F_0x2e_003005_bit_5 -F_0x2e_003005_bit_4 -F_0x2e_003005_bit_3 -F_0x2e_003005_bit_2 -F_0x2e_003005_bit_1 -F_0x2e_003005_bit0 -F_0x2e_003005_bit1 -F_0x2e_003005_bit2 -F_0x2e_003005_bit3 -F_0x2e_003005_bit4 -F_0x2e_003005_bit5 -F_0x2e_003005_bit6 -F_0x2e_003005_bit7 -F_0x2e_003005_bit8 -F_0x2e_003005_bit9 -F_0x2e_003005_bit10 -F_0x2e_003005_bit11 -F_0x2e_003005_bit12 -F_0x2e_004005_bit_7 -F_0x2e_004005_bit_6 -F_0x2e_004005_bit_5 -F_0x2e_004005_bit_4 -F_0x2e_004005_bit_3 -F_0x2e_004005_bit_2 -F_0x2e_004005_bit_1 F_0x2e_004005_bit0 F_0x2e_004005_bit1 F_0x2e_004005_bit2 -F_0x2e_004005_bit3 -F_0x2e_004005_bit4 -F_0x2e_004005_bit5 -F_0x2e_004005_bit6 -F_0x2e_004005_bit7 -F_0x2e_004005_bit8 -F_0x2e_004005_bit9 -F_0x2e_004005_bit10 -F_0x2e_004005_bit11 -F_0x2e_004005_bit12 -F_0x2e_004_0x2e__0x2e__0x2e__bit_7 -F_0x2e_004_0x2e__0x2e__0x2e__bit_6 -F_0x2e_004_0x2e__0x2e__0x2e__bit_5 -F_0x2e_004_0x2e__0x2e__0x2e__bit_4 -F_0x2e_004_0x2e__0x2e__0x2e__bit_3 -F_0x2e_004_0x2e__0x2e__0x2e__bit_2 -F_0x2e_004_0x2e__0x2e__0x2e__bit_1 -F_0x2e_004_0x2e__0x2e__0x2e__bit0 -F_0x2e_004_0x2e__0x2e__0x2e__bit1 -F_0x2e_004_0x2e__0x2e__0x2e__bit2 -F_0x2e_004_0x2e__0x2e__0x2e__bit3 -F_0x2e_004_0x2e__0x2e__0x2e__bit4 -F_0x2e_004_0x2e__0x2e__0x2e__bit5 -F_0x2e_004_0x2e__0x2e__0x2e__bit6 -F_0x2e_004_0x2e__0x2e__0x2e__bit7 -F_0x2e_004_0x2e__0x2e__0x2e__bit8 -F_0x2e_004_0x2e__0x2e__0x2e__bit9 -F_0x2e_004_0x2e__0x2e__0x2e__bit10 -F_0x2e_004_0x2e__0x2e__0x2e__bit11 -F_0x2e_004_0x2e__0x2e__0x2e__bit12 -F_0x2e_005007_bit_7 -F_0x2e_005007_bit_6 -F_0x2e_005007_bit_5 -F_0x2e_005007_bit_4 -F_0x2e_005007_bit_3 -F_0x2e_005007_bit_2 -F_0x2e_005007_bit_1 F_0x2e_005007_bit0 F_0x2e_005007_bit1 F_0x2e_005007_bit2 -F_0x2e_005007_bit3 -F_0x2e_005007_bit4 -F_0x2e_005007_bit5 -F_0x2e_005007_bit6 -F_0x2e_005007_bit7 -F_0x2e_005007_bit8 -F_0x2e_005007_bit9 -F_0x2e_005007_bit10 -F_0x2e_005007_bit11 -F_0x2e_005007_bit12 -F_0x2e_006007_bit_7 -F_0x2e_006007_bit_6 -F_0x2e_006007_bit_5 -F_0x2e_006007_bit_4 -F_0x2e_006007_bit_3 -F_0x2e_006007_bit_2 -F_0x2e_006007_bit_1 -F_0x2e_006007_bit0 -F_0x2e_006007_bit1 F_0x2e_006007_bit2 -F_0x2e_006007_bit3 -F_0x2e_006007_bit4 -F_0x2e_006007_bit5 -F_0x2e_006007_bit6 -F_0x2e_006007_bit7 -F_0x2e_006007_bit8 -F_0x2e_006007_bit9 -F_0x2e_006007_bit10 -F_0x2e_006007_bit11 -F_0x2e_006007_bit12 -F_0x2e_007008_bit_7 -F_0x2e_007008_bit_6 -F_0x2e_007008_bit_5 -F_0x2e_007008_bit_4 -F_0x2e_007008_bit_3 -F_0x2e_007008_bit_2 -F_0x2e_007008_bit_1 -F_0x2e_007008_bit0 -F_0x2e_007008_bit1 F_0x2e_007008_bit2 F_0x2e_007008_bit3 -F_0x2e_007008_bit4 -F_0x2e_007008_bit5 -F_0x2e_007008_bit6 -F_0x2e_007008_bit7 -F_0x2e_007008_bit8 -F_0x2e_007008_bit9 -F_0x2e_007008_bit10 -F_0x2e_007008_bit11 -F_0x2e_007008_bit12 -F_0x2e_008_0x2e__0x2e__0x2e__bit_7 -F_0x2e_008_0x2e__0x2e__0x2e__bit_6 -F_0x2e_008_0x2e__0x2e__0x2e__bit_5 -F_0x2e_008_0x2e__0x2e__0x2e__bit_4 -F_0x2e_008_0x2e__0x2e__0x2e__bit_3 -F_0x2e_008_0x2e__0x2e__0x2e__bit_2 -F_0x2e_008_0x2e__0x2e__0x2e__bit_1 -F_0x2e_008_0x2e__0x2e__0x2e__bit0 -F_0x2e_008_0x2e__0x2e__0x2e__bit1 F_0x2e_008_0x2e__0x2e__0x2e__bit2 F_0x2e_008_0x2e__0x2e__0x2e__bit3 -F_0x2e_008_0x2e__0x2e__0x2e__bit4 -F_0x2e_008_0x2e__0x2e__0x2e__bit5 -F_0x2e_008_0x2e__0x2e__0x2e__bit6 -F_0x2e_008_0x2e__0x2e__0x2e__bit7 -F_0x2e_008_0x2e__0x2e__0x2e__bit8 -F_0x2e_008_0x2e__0x2e__0x2e__bit9 -F_0x2e_008_0x2e__0x2e__0x2e__bit10 -F_0x2e_008_0x2e__0x2e__0x2e__bit11 -F_0x2e_008_0x2e__0x2e__0x2e__bit12 -F_0x2e_008009_bit_7 -F_0x2e_008009_bit_6 -F_0x2e_008009_bit_5 -F_0x2e_008009_bit_4 -F_0x2e_008009_bit_3 -F_0x2e_008009_bit_2 -F_0x2e_008009_bit_1 -F_0x2e_008009_bit0 -F_0x2e_008009_bit1 -F_0x2e_008009_bit2 -F_0x2e_008009_bit3 -F_0x2e_008009_bit4 -F_0x2e_008009_bit5 -F_0x2e_008009_bit6 -F_0x2e_008009_bit7 -F_0x2e_008009_bit8 -F_0x2e_008009_bit9 -F_0x2e_008009_bit10 -F_0x2e_008009_bit11 -F_0x2e_008009_bit12 -F_0x2e_010012_bit_7 -F_0x2e_010012_bit_6 -F_0x2e_010012_bit_5 -F_0x2e_010012_bit_4 -F_0x2e_010012_bit_3 -F_0x2e_010012_bit_2 -F_0x2e_010012_bit_1 F_0x2e_010012_bit0 -F_0x2e_010012_bit1 -F_0x2e_010012_bit2 -F_0x2e_010012_bit3 -F_0x2e_010012_bit4 -F_0x2e_010012_bit5 -F_0x2e_010012_bit6 -F_0x2e_010012_bit7 -F_0x2e_010012_bit8 -F_0x2e_010012_bit9 -F_0x2e_010012_bit10 -F_0x2e_010012_bit11 -F_0x2e_010012_bit12 -F_0x2e_012_0x2e__0x2e__0x2e__bit_7 -F_0x2e_012_0x2e__0x2e__0x2e__bit_6 -F_0x2e_012_0x2e__0x2e__0x2e__bit_5 -F_0x2e_012_0x2e__0x2e__0x2e__bit_4 -F_0x2e_012_0x2e__0x2e__0x2e__bit_3 -F_0x2e_012_0x2e__0x2e__0x2e__bit_2 -F_0x2e_012_0x2e__0x2e__0x2e__bit_1 -F_0x2e_012_0x2e__0x2e__0x2e__bit0 -F_0x2e_012_0x2e__0x2e__0x2e__bit1 -F_0x2e_012_0x2e__0x2e__0x2e__bit2 -F_0x2e_012_0x2e__0x2e__0x2e__bit3 -F_0x2e_012_0x2e__0x2e__0x2e__bit4 -F_0x2e_012_0x2e__0x2e__0x2e__bit5 -F_0x2e_012_0x2e__0x2e__0x2e__bit6 -F_0x2e_012_0x2e__0x2e__0x2e__bit7 -F_0x2e_012_0x2e__0x2e__0x2e__bit8 -F_0x2e_012_0x2e__0x2e__0x2e__bit9 -F_0x2e_012_0x2e__0x2e__0x2e__bit10 -F_0x2e_012_0x2e__0x2e__0x2e__bit11 -F_0x2e_012_0x2e__0x2e__0x2e__bit12 -F_0x2e_012013_bit_7 -F_0x2e_012013_bit_6 -F_0x2e_012013_bit_5 -F_0x2e_012013_bit_4 -F_0x2e_012013_bit_3 -F_0x2e_012013_bit_2 -F_0x2e_012013_bit_1 -F_0x2e_012013_bit0 F_0x2e_012013_bit1 F_0x2e_012013_bit2 -F_0x2e_012013_bit3 F_0x2e_012013_bit4 -F_0x2e_012013_bit5 -F_0x2e_012013_bit6 -F_0x2e_012013_bit7 -F_0x2e_012013_bit8 -F_0x2e_012013_bit9 -F_0x2e_012013_bit10 -F_0x2e_012013_bit11 -F_0x2e_012013_bit12 -F_0x2e_013016_bit_7 -F_0x2e_013016_bit_6 -F_0x2e_013016_bit_5 -F_0x2e_013016_bit_4 -F_0x2e_013016_bit_3 -F_0x2e_013016_bit_2 -F_0x2e_013016_bit_1 -F_0x2e_013016_bit0 F_0x2e_013016_bit1 -F_0x2e_013016_bit2 F_0x2e_013016_bit3 F_0x2e_013016_bit4 -F_0x2e_013016_bit5 -F_0x2e_013016_bit6 -F_0x2e_013016_bit7 -F_0x2e_013016_bit8 -F_0x2e_013016_bit9 -F_0x2e_013016_bit10 -F_0x2e_013016_bit11 -F_0x2e_013016_bit12 -F_0x2e_014015_bit_7 -F_0x2e_014015_bit_6 -F_0x2e_014015_bit_5 -F_0x2e_014015_bit_4 -F_0x2e_014015_bit_3 -F_0x2e_014015_bit_2 -F_0x2e_014015_bit_1 -F_0x2e_014015_bit0 -F_0x2e_014015_bit1 -F_0x2e_014015_bit2 -F_0x2e_014015_bit3 -F_0x2e_014015_bit4 -F_0x2e_014015_bit5 -F_0x2e_014015_bit6 -F_0x2e_014015_bit7 -F_0x2e_014015_bit8 -F_0x2e_014015_bit9 -F_0x2e_014015_bit10 -F_0x2e_014015_bit11 -F_0x2e_014015_bit12 -F_0x2e_015016_bit_7 -F_0x2e_015016_bit_6 -F_0x2e_015016_bit_5 -F_0x2e_015016_bit_4 -F_0x2e_015016_bit_3 -F_0x2e_015016_bit_2 -F_0x2e_015016_bit_1 F_0x2e_015016_bit0 -F_0x2e_015016_bit1 -F_0x2e_015016_bit2 -F_0x2e_015016_bit3 -F_0x2e_015016_bit4 -F_0x2e_015016_bit5 -F_0x2e_015016_bit6 -F_0x2e_015016_bit7 -F_0x2e_015016_bit8 -F_0x2e_015016_bit9 -F_0x2e_015016_bit10 -F_0x2e_015016_bit11 -F_0x2e_015016_bit12 -F_0x2e_016_0x2e__0x2e__0x2e__bit_7 -F_0x2e_016_0x2e__0x2e__0x2e__bit_6 -F_0x2e_016_0x2e__0x2e__0x2e__bit_5 -F_0x2e_016_0x2e__0x2e__0x2e__bit_4 -F_0x2e_016_0x2e__0x2e__0x2e__bit_3 -F_0x2e_016_0x2e__0x2e__0x2e__bit_2 -F_0x2e_016_0x2e__0x2e__0x2e__bit_1 F_0x2e_016_0x2e__0x2e__0x2e__bit0 F_0x2e_016_0x2e__0x2e__0x2e__bit1 -F_0x2e_016_0x2e__0x2e__0x2e__bit2 F_0x2e_016_0x2e__0x2e__0x2e__bit3 F_0x2e_016_0x2e__0x2e__0x2e__bit4 -F_0x2e_016_0x2e__0x2e__0x2e__bit5 -F_0x2e_016_0x2e__0x2e__0x2e__bit6 -F_0x2e_016_0x2e__0x2e__0x2e__bit7 -F_0x2e_016_0x2e__0x2e__0x2e__bit8 -F_0x2e_016_0x2e__0x2e__0x2e__bit9 -F_0x2e_016_0x2e__0x2e__0x2e__bit10 -F_0x2e_016_0x2e__0x2e__0x2e__bit11 -F_0x2e_016_0x2e__0x2e__0x2e__bit12 -F_0x2e_016017_bit_7 -F_0x2e_016017_bit_6 -F_0x2e_016017_bit_5 -F_0x2e_016017_bit_4 -F_0x2e_016017_bit_3 -F_0x2e_016017_bit_2 -F_0x2e_016017_bit_1 -F_0x2e_016017_bit0 -F_0x2e_016017_bit1 -F_0x2e_016017_bit2 -F_0x2e_016017_bit3 -F_0x2e_016017_bit4 -F_0x2e_016017_bit5 -F_0x2e_016017_bit6 -F_0x2e_016017_bit7 -F_0x2e_016017_bit8 -F_0x2e_016017_bit9 -F_0x2e_016017_bit10 -F_0x2e_016017_bit11 -F_0x2e_016017_bit12 -F_0x2e_017018_bit_7 -F_0x2e_017018_bit_6 -F_0x2e_017018_bit_5 -F_0x2e_017018_bit_4 -F_0x2e_017018_bit_3 -F_0x2e_017018_bit_2 -F_0x2e_017018_bit_1 -F_0x2e_017018_bit0 -F_0x2e_017018_bit1 -F_0x2e_017018_bit2 -F_0x2e_017018_bit3 -F_0x2e_017018_bit4 -F_0x2e_017018_bit5 -F_0x2e_017018_bit6 -F_0x2e_017018_bit7 -F_0x2e_017018_bit8 -F_0x2e_017018_bit9 -F_0x2e_017018_bit10 -F_0x2e_017018_bit11 -F_0x2e_017018_bit12 -F_0x2e_009018_bit_7 -F_0x2e_009018_bit_6 -F_0x2e_009018_bit_5 -F_0x2e_009018_bit_4 -F_0x2e_009018_bit_3 -F_0x2e_009018_bit_2 -F_0x2e_009018_bit_1 -F_0x2e_009018_bit0 -F_0x2e_009018_bit1 -F_0x2e_009018_bit2 -F_0x2e_009018_bit3 -F_0x2e_009018_bit4 -F_0x2e_009018_bit5 -F_0x2e_009018_bit6 -F_0x2e_009018_bit7 -F_0x2e_009018_bit8 -F_0x2e_009018_bit9 -F_0x2e_009018_bit10 -F_0x2e_009018_bit11 -F_0x2e_009018_bit12 -F_0x2e_018019_bit_7 -F_0x2e_018019_bit_6 -F_0x2e_018019_bit_5 -F_0x2e_018019_bit_4 -F_0x2e_018019_bit_3 -F_0x2e_018019_bit_2 -F_0x2e_018019_bit_1 -F_0x2e_018019_bit0 -F_0x2e_018019_bit1 -F_0x2e_018019_bit2 -F_0x2e_018019_bit3 -F_0x2e_018019_bit4 -F_0x2e_018019_bit5 -F_0x2e_018019_bit6 -F_0x2e_018019_bit7 -F_0x2e_018019_bit8 -F_0x2e_018019_bit9 -F_0x2e_018019_bit10 -F_0x2e_018019_bit11 -F_0x2e_018019_bit12 -F_0x2e_019024_bit_7 -F_0x2e_019024_bit_6 -F_0x2e_019024_bit_5 -F_0x2e_019024_bit_4 -F_0x2e_019024_bit_3 -F_0x2e_019024_bit_2 -F_0x2e_019024_bit_1 -F_0x2e_019024_bit0 F_0x2e_019024_bit1 -F_0x2e_019024_bit2 -F_0x2e_019024_bit3 -F_0x2e_019024_bit4 -F_0x2e_019024_bit5 -F_0x2e_019024_bit6 -F_0x2e_019024_bit7 -F_0x2e_019024_bit8 -F_0x2e_019024_bit9 -F_0x2e_019024_bit10 -F_0x2e_019024_bit11 -F_0x2e_019024_bit12 -F_0x2e_024_0x2e__0x2e__0x2e__bit_7 -F_0x2e_024_0x2e__0x2e__0x2e__bit_6 -F_0x2e_024_0x2e__0x2e__0x2e__bit_5 -F_0x2e_024_0x2e__0x2e__0x2e__bit_4 -F_0x2e_024_0x2e__0x2e__0x2e__bit_3 -F_0x2e_024_0x2e__0x2e__0x2e__bit_2 -F_0x2e_024_0x2e__0x2e__0x2e__bit_1 -F_0x2e_024_0x2e__0x2e__0x2e__bit0 -F_0x2e_024_0x2e__0x2e__0x2e__bit1 -F_0x2e_024_0x2e__0x2e__0x2e__bit2 -F_0x2e_024_0x2e__0x2e__0x2e__bit3 -F_0x2e_024_0x2e__0x2e__0x2e__bit4 -F_0x2e_024_0x2e__0x2e__0x2e__bit5 -F_0x2e_024_0x2e__0x2e__0x2e__bit6 -F_0x2e_024_0x2e__0x2e__0x2e__bit7 -F_0x2e_024_0x2e__0x2e__0x2e__bit8 -F_0x2e_024_0x2e__0x2e__0x2e__bit9 -F_0x2e_024_0x2e__0x2e__0x2e__bit10 -F_0x2e_024_0x2e__0x2e__0x2e__bit11 -F_0x2e_024_0x2e__0x2e__0x2e__bit12 -F_0x2e_023024_bit_7 -F_0x2e_023024_bit_6 -F_0x2e_023024_bit_5 -F_0x2e_023024_bit_4 -F_0x2e_023024_bit_3 -F_0x2e_023024_bit_2 -F_0x2e_023024_bit_1 -F_0x2e_023024_bit0 -F_0x2e_023024_bit1 -F_0x2e_023024_bit2 -F_0x2e_023024_bit3 -F_0x2e_023024_bit4 -F_0x2e_023024_bit5 -F_0x2e_023024_bit6 -F_0x2e_023024_bit7 -F_0x2e_023024_bit8 -F_0x2e_023024_bit9 -F_0x2e_023024_bit10 -F_0x2e_023024_bit11 -F_0x2e_023024_bit12 -F_0x2e_022023_bit_7 -F_0x2e_022023_bit_6 -F_0x2e_022023_bit_5 -F_0x2e_022023_bit_4 -F_0x2e_022023_bit_3 -F_0x2e_022023_bit_2 -F_0x2e_022023_bit_1 -F_0x2e_022023_bit0 -F_0x2e_022023_bit1 -F_0x2e_022023_bit2 -F_0x2e_022023_bit3 -F_0x2e_022023_bit4 -F_0x2e_022023_bit5 -F_0x2e_022023_bit6 -F_0x2e_022023_bit7 -F_0x2e_022023_bit8 -F_0x2e_022023_bit9 -F_0x2e_022023_bit10 -F_0x2e_022023_bit11 -F_0x2e_022023_bit12 -F_0x2e_020022_bit_7 -F_0x2e_020022_bit_6 -F_0x2e_020022_bit_5 -F_0x2e_020022_bit_4 -F_0x2e_020022_bit_3 -F_0x2e_020022_bit_2 -F_0x2e_020022_bit_1 -F_0x2e_020022_bit0 -F_0x2e_020022_bit1 -F_0x2e_020022_bit2 -F_0x2e_020022_bit3 -F_0x2e_020022_bit4 -F_0x2e_020022_bit5 -F_0x2e_020022_bit6 -F_0x2e_020022_bit7 -F_0x2e_020022_bit8 -F_0x2e_020022_bit9 -F_0x2e_020022_bit10 -F_0x2e_020022_bit11 -F_0x2e_020022_bit12 -F_0x2e_021022_bit_7 -F_0x2e_021022_bit_6 -F_0x2e_021022_bit_5 -F_0x2e_021022_bit_4 -F_0x2e_021022_bit_3 -F_0x2e_021022_bit_2 -F_0x2e_021022_bit_1 F_0x2e_021022_bit0 F_0x2e_021022_bit1 F_0x2e_021022_bit2 -F_0x2e_021022_bit3 -F_0x2e_021022_bit4 -F_0x2e_021022_bit5 -F_0x2e_021022_bit6 -F_0x2e_021022_bit7 -F_0x2e_021022_bit8 -F_0x2e_021022_bit9 -F_0x2e_021022_bit10 -F_0x2e_021022_bit11 -F_0x2e_021022_bit12 -F_0x2e_022_0x2e__0x2e__0x2e__bit_7 -F_0x2e_022_0x2e__0x2e__0x2e__bit_6 -F_0x2e_022_0x2e__0x2e__0x2e__bit_5 -F_0x2e_022_0x2e__0x2e__0x2e__bit_4 -F_0x2e_022_0x2e__0x2e__0x2e__bit_3 -F_0x2e_022_0x2e__0x2e__0x2e__bit_2 -F_0x2e_022_0x2e__0x2e__0x2e__bit_1 F_0x2e_022_0x2e__0x2e__0x2e__bit0 F_0x2e_022_0x2e__0x2e__0x2e__bit1 F_0x2e_022_0x2e__0x2e__0x2e__bit2 -F_0x2e_022_0x2e__0x2e__0x2e__bit3 -F_0x2e_022_0x2e__0x2e__0x2e__bit4 -F_0x2e_022_0x2e__0x2e__0x2e__bit5 -F_0x2e_022_0x2e__0x2e__0x2e__bit6 -F_0x2e_022_0x2e__0x2e__0x2e__bit7 -F_0x2e_022_0x2e__0x2e__0x2e__bit8 -F_0x2e_022_0x2e__0x2e__0x2e__bit9 -F_0x2e_022_0x2e__0x2e__0x2e__bit10 -F_0x2e_022_0x2e__0x2e__0x2e__bit11 -F_0x2e_022_0x2e__0x2e__0x2e__bit12 -F_0x2e_024026_bit_7 -F_0x2e_024026_bit_6 -F_0x2e_024026_bit_5 -F_0x2e_024026_bit_4 -F_0x2e_024026_bit_3 -F_0x2e_024026_bit_2 -F_0x2e_024026_bit_1 -F_0x2e_024026_bit0 F_0x2e_024026_bit1 -F_0x2e_024026_bit2 -F_0x2e_024026_bit3 -F_0x2e_024026_bit4 -F_0x2e_024026_bit5 -F_0x2e_024026_bit6 -F_0x2e_024026_bit7 -F_0x2e_024026_bit8 -F_0x2e_024026_bit9 -F_0x2e_024026_bit10 -F_0x2e_024026_bit11 -F_0x2e_024026_bit12 -F_0x2e_025026_bit_7 -F_0x2e_025026_bit_6 -F_0x2e_025026_bit_5 -F_0x2e_025026_bit_4 -F_0x2e_025026_bit_3 -F_0x2e_025026_bit_2 -F_0x2e_025026_bit_1 F_0x2e_025026_bit0 F_0x2e_025026_bit1 -F_0x2e_025026_bit2 -F_0x2e_025026_bit3 F_0x2e_025026_bit4 -F_0x2e_025026_bit5 -F_0x2e_025026_bit6 -F_0x2e_025026_bit7 -F_0x2e_025026_bit8 -F_0x2e_025026_bit9 -F_0x2e_025026_bit10 -F_0x2e_025026_bit11 -F_0x2e_025026_bit12 -F_0x2e_025_0x2e__0x2e__0x2e__bit_7 -F_0x2e_025_0x2e__0x2e__0x2e__bit_6 -F_0x2e_025_0x2e__0x2e__0x2e__bit_5 -F_0x2e_025_0x2e__0x2e__0x2e__bit_4 -F_0x2e_025_0x2e__0x2e__0x2e__bit_3 -F_0x2e_025_0x2e__0x2e__0x2e__bit_2 -F_0x2e_025_0x2e__0x2e__0x2e__bit_1 -F_0x2e_025_0x2e__0x2e__0x2e__bit0 -F_0x2e_025_0x2e__0x2e__0x2e__bit1 -F_0x2e_025_0x2e__0x2e__0x2e__bit2 -F_0x2e_025_0x2e__0x2e__0x2e__bit3 -F_0x2e_025_0x2e__0x2e__0x2e__bit4 -F_0x2e_025_0x2e__0x2e__0x2e__bit5 -F_0x2e_025_0x2e__0x2e__0x2e__bit6 -F_0x2e_025_0x2e__0x2e__0x2e__bit7 -F_0x2e_025_0x2e__0x2e__0x2e__bit8 -F_0x2e_025_0x2e__0x2e__0x2e__bit9 -F_0x2e_025_0x2e__0x2e__0x2e__bit10 -F_0x2e_025_0x2e__0x2e__0x2e__bit11 -F_0x2e_025_0x2e__0x2e__0x2e__bit12 -F_0x2e_026027_bit_7 -F_0x2e_026027_bit_6 -F_0x2e_026027_bit_5 -F_0x2e_026027_bit_4 -F_0x2e_026027_bit_3 -F_0x2e_026027_bit_2 -F_0x2e_026027_bit_1 F_0x2e_026027_bit0 F_0x2e_026027_bit1 F_0x2e_026027_bit2 F_0x2e_026027_bit3 F_0x2e_026027_bit4 -F_0x2e_026027_bit5 -F_0x2e_026027_bit6 -F_0x2e_026027_bit7 -F_0x2e_026027_bit8 -F_0x2e_026027_bit9 -F_0x2e_026027_bit10 -F_0x2e_026027_bit11 -F_0x2e_026027_bit12 -F_0x2e_027_0x2e__0x2e__0x2e__bit_7 -F_0x2e_027_0x2e__0x2e__0x2e__bit_6 -F_0x2e_027_0x2e__0x2e__0x2e__bit_5 -F_0x2e_027_0x2e__0x2e__0x2e__bit_4 -F_0x2e_027_0x2e__0x2e__0x2e__bit_3 -F_0x2e_027_0x2e__0x2e__0x2e__bit_2 -F_0x2e_027_0x2e__0x2e__0x2e__bit_1 -F_0x2e_027_0x2e__0x2e__0x2e__bit0 -F_0x2e_027_0x2e__0x2e__0x2e__bit1 -F_0x2e_027_0x2e__0x2e__0x2e__bit2 -F_0x2e_027_0x2e__0x2e__0x2e__bit3 -F_0x2e_027_0x2e__0x2e__0x2e__bit4 -F_0x2e_027_0x2e__0x2e__0x2e__bit5 -F_0x2e_027_0x2e__0x2e__0x2e__bit6 -F_0x2e_027_0x2e__0x2e__0x2e__bit7 -F_0x2e_027_0x2e__0x2e__0x2e__bit8 -F_0x2e_027_0x2e__0x2e__0x2e__bit9 -F_0x2e_027_0x2e__0x2e__0x2e__bit10 -F_0x2e_027_0x2e__0x2e__0x2e__bit11 -F_0x2e_027_0x2e__0x2e__0x2e__bit12 -F_0x2e_027032_bit_7 -F_0x2e_027032_bit_6 -F_0x2e_027032_bit_5 -F_0x2e_027032_bit_4 -F_0x2e_027032_bit_3 -F_0x2e_027032_bit_2 -F_0x2e_027032_bit_1 F_0x2e_027032_bit0 F_0x2e_027032_bit1 F_0x2e_027032_bit2 F_0x2e_027032_bit3 F_0x2e_027032_bit4 -F_0x2e_027032_bit5 -F_0x2e_027032_bit6 -F_0x2e_027032_bit7 -F_0x2e_027032_bit8 -F_0x2e_027032_bit9 -F_0x2e_027032_bit10 -F_0x2e_027032_bit11 -F_0x2e_027032_bit12 -F_0x2e_030031_bit_7 -F_0x2e_030031_bit_6 -F_0x2e_030031_bit_5 -F_0x2e_030031_bit_4 -F_0x2e_030031_bit_3 -F_0x2e_030031_bit_2 -F_0x2e_030031_bit_1 -F_0x2e_030031_bit0 -F_0x2e_030031_bit1 -F_0x2e_030031_bit2 -F_0x2e_030031_bit3 -F_0x2e_030031_bit4 -F_0x2e_030031_bit5 -F_0x2e_030031_bit6 -F_0x2e_030031_bit7 -F_0x2e_030031_bit8 -F_0x2e_030031_bit9 -F_0x2e_030031_bit10 -F_0x2e_030031_bit11 -F_0x2e_030031_bit12 -F_0x2e_031032_bit_7 -F_0x2e_031032_bit_6 -F_0x2e_031032_bit_5 -F_0x2e_031032_bit_4 -F_0x2e_031032_bit_3 -F_0x2e_031032_bit_2 -F_0x2e_031032_bit_1 F_0x2e_031032_bit0 -F_0x2e_031032_bit1 F_0x2e_031032_bit2 -F_0x2e_031032_bit3 -F_0x2e_031032_bit4 -F_0x2e_031032_bit5 -F_0x2e_031032_bit6 -F_0x2e_031032_bit7 -F_0x2e_031032_bit8 -F_0x2e_031032_bit9 -F_0x2e_031032_bit10 -F_0x2e_031032_bit11 -F_0x2e_031032_bit12 -F_0x2e_029031_bit_7 -F_0x2e_029031_bit_6 -F_0x2e_029031_bit_5 -F_0x2e_029031_bit_4 -F_0x2e_029031_bit_3 -F_0x2e_029031_bit_2 -F_0x2e_029031_bit_1 F_0x2e_029031_bit0 -F_0x2e_029031_bit1 F_0x2e_029031_bit2 -F_0x2e_029031_bit3 -F_0x2e_029031_bit4 -F_0x2e_029031_bit5 -F_0x2e_029031_bit6 -F_0x2e_029031_bit7 -F_0x2e_029031_bit8 -F_0x2e_029031_bit9 -F_0x2e_029031_bit10 -F_0x2e_029031_bit11 -F_0x2e_029031_bit12 -F_0x2e_028029_bit_7 -F_0x2e_028029_bit_6 -F_0x2e_028029_bit_5 -F_0x2e_028029_bit_4 -F_0x2e_028029_bit_3 -F_0x2e_028029_bit_2 -F_0x2e_028029_bit_1 -F_0x2e_028029_bit0 -F_0x2e_028029_bit1 -F_0x2e_028029_bit2 -F_0x2e_028029_bit3 -F_0x2e_028029_bit4 -F_0x2e_028029_bit5 -F_0x2e_028029_bit6 -F_0x2e_028029_bit7 -F_0x2e_028029_bit8 -F_0x2e_028029_bit9 -F_0x2e_028029_bit10 -F_0x2e_028029_bit11 -F_0x2e_028029_bit12 -F_0x2e_028_0x2e__0x2e__0x2e__bit_7 -F_0x2e_028_0x2e__0x2e__0x2e__bit_6 -F_0x2e_028_0x2e__0x2e__0x2e__bit_5 -F_0x2e_028_0x2e__0x2e__0x2e__bit_4 -F_0x2e_028_0x2e__0x2e__0x2e__bit_3 -F_0x2e_028_0x2e__0x2e__0x2e__bit_2 -F_0x2e_028_0x2e__0x2e__0x2e__bit_1 -F_0x2e_028_0x2e__0x2e__0x2e__bit0 -F_0x2e_028_0x2e__0x2e__0x2e__bit1 -F_0x2e_028_0x2e__0x2e__0x2e__bit2 -F_0x2e_028_0x2e__0x2e__0x2e__bit3 -F_0x2e_028_0x2e__0x2e__0x2e__bit4 -F_0x2e_028_0x2e__0x2e__0x2e__bit5 -F_0x2e_028_0x2e__0x2e__0x2e__bit6 -F_0x2e_028_0x2e__0x2e__0x2e__bit7 -F_0x2e_028_0x2e__0x2e__0x2e__bit8 -F_0x2e_028_0x2e__0x2e__0x2e__bit9 -F_0x2e_028_0x2e__0x2e__0x2e__bit10 -F_0x2e_028_0x2e__0x2e__0x2e__bit11 -F_0x2e_028_0x2e__0x2e__0x2e__bit12 -F_0x2e_032033_bit_7 -F_0x2e_032033_bit_6 -F_0x2e_032033_bit_5 -F_0x2e_032033_bit_4 -F_0x2e_032033_bit_3 -F_0x2e_032033_bit_2 -F_0x2e_032033_bit_1 -F_0x2e_032033_bit0 -F_0x2e_032033_bit1 F_0x2e_032033_bit2 -F_0x2e_032033_bit3 -F_0x2e_032033_bit4 F_0x2e_032033_bit5 -F_0x2e_032033_bit6 -F_0x2e_032033_bit7 -F_0x2e_032033_bit8 -F_0x2e_032033_bit9 -F_0x2e_032033_bit10 -F_0x2e_032033_bit11 -F_0x2e_032033_bit12 -F_0x2e_033037_bit_7 -F_0x2e_033037_bit_6 -F_0x2e_033037_bit_5 -F_0x2e_033037_bit_4 -F_0x2e_033037_bit_3 -F_0x2e_033037_bit_2 -F_0x2e_033037_bit_1 -F_0x2e_033037_bit0 -F_0x2e_033037_bit1 F_0x2e_033037_bit2 -F_0x2e_033037_bit3 -F_0x2e_033037_bit4 F_0x2e_033037_bit5 -F_0x2e_033037_bit6 -F_0x2e_033037_bit7 -F_0x2e_033037_bit8 -F_0x2e_033037_bit9 -F_0x2e_033037_bit10 -F_0x2e_033037_bit11 -F_0x2e_033037_bit12 -F_0x2e_034036_bit_7 -F_0x2e_034036_bit_6 -F_0x2e_034036_bit_5 -F_0x2e_034036_bit_4 -F_0x2e_034036_bit_3 -F_0x2e_034036_bit_2 -F_0x2e_034036_bit_1 -F_0x2e_034036_bit0 -F_0x2e_034036_bit1 -F_0x2e_034036_bit2 -F_0x2e_034036_bit3 -F_0x2e_034036_bit4 -F_0x2e_034036_bit5 -F_0x2e_034036_bit6 -F_0x2e_034036_bit7 -F_0x2e_034036_bit8 -F_0x2e_034036_bit9 -F_0x2e_034036_bit10 -F_0x2e_034036_bit11 -F_0x2e_034036_bit12 -F_0x2e_035036_bit_7 -F_0x2e_035036_bit_6 -F_0x2e_035036_bit_5 -F_0x2e_035036_bit_4 -F_0x2e_035036_bit_3 -F_0x2e_035036_bit_2 -F_0x2e_035036_bit_1 -F_0x2e_035036_bit0 -F_0x2e_035036_bit1 -F_0x2e_035036_bit2 -F_0x2e_035036_bit3 -F_0x2e_035036_bit4 -F_0x2e_035036_bit5 -F_0x2e_035036_bit6 -F_0x2e_035036_bit7 -F_0x2e_035036_bit8 -F_0x2e_035036_bit9 -F_0x2e_035036_bit10 -F_0x2e_035036_bit11 -F_0x2e_035036_bit12 -F_0x2e_037038_bit_7 -F_0x2e_037038_bit_6 -F_0x2e_037038_bit_5 -F_0x2e_037038_bit_4 -F_0x2e_037038_bit_3 -F_0x2e_037038_bit_2 -F_0x2e_037038_bit_1 -F_0x2e_037038_bit0 -F_0x2e_037038_bit1 F_0x2e_037038_bit2 -F_0x2e_037038_bit3 -F_0x2e_037038_bit4 F_0x2e_037038_bit5 -F_0x2e_037038_bit6 -F_0x2e_037038_bit7 -F_0x2e_037038_bit8 -F_0x2e_037038_bit9 -F_0x2e_037038_bit10 -F_0x2e_037038_bit11 -F_0x2e_037038_bit12 -F_0x2e_039040_bit_7 -F_0x2e_039040_bit_6 -F_0x2e_039040_bit_5 -F_0x2e_039040_bit_4 -F_0x2e_039040_bit_3 -F_0x2e_039040_bit_2 -F_0x2e_039040_bit_1 F_0x2e_039040_bit0 -F_0x2e_039040_bit1 F_0x2e_039040_bit2 -F_0x2e_039040_bit3 -F_0x2e_039040_bit4 -F_0x2e_039040_bit5 -F_0x2e_039040_bit6 -F_0x2e_039040_bit7 -F_0x2e_039040_bit8 -F_0x2e_039040_bit9 -F_0x2e_039040_bit10 -F_0x2e_039040_bit11 -F_0x2e_039040_bit12 -F_0x2e_040_0x2e__0x2e__0x2e__bit_7 -F_0x2e_040_0x2e__0x2e__0x2e__bit_6 -F_0x2e_040_0x2e__0x2e__0x2e__bit_5 -F_0x2e_040_0x2e__0x2e__0x2e__bit_4 -F_0x2e_040_0x2e__0x2e__0x2e__bit_3 -F_0x2e_040_0x2e__0x2e__0x2e__bit_2 -F_0x2e_040_0x2e__0x2e__0x2e__bit_1 -F_0x2e_040_0x2e__0x2e__0x2e__bit0 -F_0x2e_040_0x2e__0x2e__0x2e__bit1 -F_0x2e_040_0x2e__0x2e__0x2e__bit2 -F_0x2e_040_0x2e__0x2e__0x2e__bit3 -F_0x2e_040_0x2e__0x2e__0x2e__bit4 -F_0x2e_040_0x2e__0x2e__0x2e__bit5 -F_0x2e_040_0x2e__0x2e__0x2e__bit6 -F_0x2e_040_0x2e__0x2e__0x2e__bit7 -F_0x2e_040_0x2e__0x2e__0x2e__bit8 -F_0x2e_040_0x2e__0x2e__0x2e__bit9 -F_0x2e_040_0x2e__0x2e__0x2e__bit10 -F_0x2e_040_0x2e__0x2e__0x2e__bit11 -F_0x2e_040_0x2e__0x2e__0x2e__bit12 -F_0x2e_041_0x2e__0x2e__0x2e__bit_7 -F_0x2e_041_0x2e__0x2e__0x2e__bit_6 -F_0x2e_041_0x2e__0x2e__0x2e__bit_5 -F_0x2e_041_0x2e__0x2e__0x2e__bit_4 -F_0x2e_041_0x2e__0x2e__0x2e__bit_3 -F_0x2e_041_0x2e__0x2e__0x2e__bit_2 -F_0x2e_041_0x2e__0x2e__0x2e__bit_1 -F_0x2e_041_0x2e__0x2e__0x2e__bit0 -F_0x2e_041_0x2e__0x2e__0x2e__bit1 -F_0x2e_041_0x2e__0x2e__0x2e__bit2 -F_0x2e_041_0x2e__0x2e__0x2e__bit3 -F_0x2e_041_0x2e__0x2e__0x2e__bit4 -F_0x2e_041_0x2e__0x2e__0x2e__bit5 -F_0x2e_041_0x2e__0x2e__0x2e__bit6 -F_0x2e_041_0x2e__0x2e__0x2e__bit7 -F_0x2e_041_0x2e__0x2e__0x2e__bit8 -F_0x2e_041_0x2e__0x2e__0x2e__bit9 -F_0x2e_041_0x2e__0x2e__0x2e__bit10 -F_0x2e_041_0x2e__0x2e__0x2e__bit11 -F_0x2e_041_0x2e__0x2e__0x2e__bit12 -F_0x2e_040041_bit_7 -F_0x2e_040041_bit_6 -F_0x2e_040041_bit_5 -F_0x2e_040041_bit_4 -F_0x2e_040041_bit_3 -F_0x2e_040041_bit_2 -F_0x2e_040041_bit_1 -F_0x2e_040041_bit0 F_0x2e_040041_bit1 F_0x2e_040041_bit2 F_0x2e_040041_bit3 -F_0x2e_040041_bit4 F_0x2e_040041_bit5 -F_0x2e_040041_bit6 -F_0x2e_040041_bit7 -F_0x2e_040041_bit8 -F_0x2e_040041_bit9 -F_0x2e_040041_bit10 -F_0x2e_040041_bit11 -F_0x2e_040041_bit12 -F_0x2e_041042_bit_7 -F_0x2e_041042_bit_6 -F_0x2e_041042_bit_5 -F_0x2e_041042_bit_4 -F_0x2e_041042_bit_3 -F_0x2e_041042_bit_2 -F_0x2e_041042_bit_1 F_0x2e_041042_bit0 F_0x2e_041042_bit1 -F_0x2e_041042_bit2 -F_0x2e_041042_bit3 F_0x2e_041042_bit4 F_0x2e_041042_bit5 -F_0x2e_041042_bit6 -F_0x2e_041042_bit7 -F_0x2e_041042_bit8 -F_0x2e_041042_bit9 -F_0x2e_041042_bit10 -F_0x2e_041042_bit11 -F_0x2e_041042_bit12 -F_0x2e_042_0x2e__0x2e__0x2e__bit_7 -F_0x2e_042_0x2e__0x2e__0x2e__bit_6 -F_0x2e_042_0x2e__0x2e__0x2e__bit_5 -F_0x2e_042_0x2e__0x2e__0x2e__bit_4 -F_0x2e_042_0x2e__0x2e__0x2e__bit_3 -F_0x2e_042_0x2e__0x2e__0x2e__bit_2 -F_0x2e_042_0x2e__0x2e__0x2e__bit_1 F_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_042_0x2e__0x2e__0x2e__bit1 -F_0x2e_042_0x2e__0x2e__0x2e__bit2 F_0x2e_042_0x2e__0x2e__0x2e__bit3 F_0x2e_042_0x2e__0x2e__0x2e__bit4 F_0x2e_042_0x2e__0x2e__0x2e__bit5 -F_0x2e_042_0x2e__0x2e__0x2e__bit6 -F_0x2e_042_0x2e__0x2e__0x2e__bit7 -F_0x2e_042_0x2e__0x2e__0x2e__bit8 -F_0x2e_042_0x2e__0x2e__0x2e__bit9 -F_0x2e_042_0x2e__0x2e__0x2e__bit10 -F_0x2e_042_0x2e__0x2e__0x2e__bit11 -F_0x2e_042_0x2e__0x2e__0x2e__bit12 -F_0x2e_011012_bit_7 -F_0x2e_011012_bit_6 -F_0x2e_011012_bit_5 -F_0x2e_011012_bit_4 -F_0x2e_011012_bit_3 -F_0x2e_011012_bit_2 -F_0x2e_011012_bit_1 F_0x2e_011012_bit0 -F_0x2e_011012_bit1 F_0x2e_011012_bit2 -F_0x2e_011012_bit3 F_0x2e_011012_bit4 -F_0x2e_011012_bit5 -F_0x2e_011012_bit6 -F_0x2e_011012_bit7 -F_0x2e_011012_bit8 -F_0x2e_011012_bit9 -F_0x2e_011012_bit10 -F_0x2e_011012_bit11 -F_0x2e_011012_bit12 -F_0x2e_036037_bit_7 -F_0x2e_036037_bit_6 -F_0x2e_036037_bit_5 -F_0x2e_036037_bit_4 -F_0x2e_036037_bit_3 -F_0x2e_036037_bit_2 -F_0x2e_036037_bit_1 -F_0x2e_036037_bit0 -F_0x2e_036037_bit1 -F_0x2e_036037_bit2 -F_0x2e_036037_bit3 -F_0x2e_036037_bit4 -F_0x2e_036037_bit5 -F_0x2e_036037_bit6 -F_0x2e_036037_bit7 -F_0x2e_036037_bit8 -F_0x2e_036037_bit9 -F_0x2e_036037_bit10 -F_0x2e_036037_bit11 -F_0x2e_036037_bit12 -F_0x2e_038040_bit_7 -F_0x2e_038040_bit_6 -F_0x2e_038040_bit_5 -F_0x2e_038040_bit_4 -F_0x2e_038040_bit_3 -F_0x2e_038040_bit_2 -F_0x2e_038040_bit_1 F_0x2e_038040_bit0 -F_0x2e_038040_bit1 -F_0x2e_038040_bit2 F_0x2e_038040_bit3 -F_0x2e_038040_bit4 F_0x2e_038040_bit5 -F_0x2e_038040_bit6 -F_0x2e_038040_bit7 -F_0x2e_038040_bit8 -F_0x2e_038040_bit9 -F_0x2e_038040_bit10 -F_0x2e_038040_bit11 -F_0x2e_038040_bit12
c _______________________________________________________________________________
c 
c restarts              : 109
c conflicts             : 37627          (34 /sec)
c decisions             : 85147          (77 /sec)
c propagations          : 274972014      (248036 /sec)
c inspects              : 1029485597     (928640 /sec)
c CPU time              : 1108.6 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.95 2/54 23291
Raw data (stat): 23291 (runsolver) R 23290 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547253069 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.99974 s]
Raw data (loadavg): 0.87 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 14548 0 0 0 954 44 0 0 25 0 1 0 547253069 66039808 13724 4294967295 134512640 134672761 3221224544 3221222548 1075351063 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16123 13724 603 41 0 16082 0
vsize: 64492
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 17253 0 0 0 1918 54 0 0 25 0 1 0 547253069 73588736 15395 4294967295 134512640 134672761 3221224544 3221223040 134618816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17966 15395 603 41 0 17925 0
vsize: 71864
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 26448 0 0 0 2885 86 0 0 25 0 1 0 547253069 102182912 20530 4294967295 134512640 134672761 3221224544 3221223036 134642749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24947 20530 603 41 0 24906 0
vsize: 99788
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 27370 0 0 0 3882 89 0 0 25 0 1 0 547253069 96030720 19548 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23445 19548 603 41 0 23404 0
vsize: 93780
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 39553 0 0 0 4849 122 0 0 25 0 1 0 547253069 124465152 27042 4294967295 134512640 134672761 3221224544 3221223088 134621081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30387 27042 603 41 0 30346 0
vsize: 121548
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 44516 0 0 0 5826 145 0 0 25 0 1 0 547253069 131178496 27990 4294967295 134512640 134672761 3221224544 3221222880 134605503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32026 27990 603 41 0 31985 0
vsize: 128104
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 49447 0 0 0 6807 163 0 0 25 0 1 0 547253069 117383168 25828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28658 25828 603 41 0 28617 0
vsize: 114632
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 49476 0 0 0 7807 163 0 0 25 0 1 0 547253069 117510144 25857 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28689 25857 603 41 0 28648 0
vsize: 114756
[startup+90.0032 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 49500 0 0 0 8807 164 0 0 25 0 1 0 547253069 117645312 25881 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28722 25881 603 41 0 28681 0
vsize: 114888
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 57804 0 0 0 9780 190 0 0 25 0 1 0 547253069 117723136 25958 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28741 25958 603 41 0 28700 0
vsize: 114964
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 66254 0 0 0 10754 216 0 0 25 0 1 0 547253069 117772288 25988 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28753 25988 603 41 0 28712 0
vsize: 115012
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 66295 0 0 0 11754 216 0 0 25 0 1 0 547253069 118026240 26029 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28815 26029 603 41 0 28774 0
vsize: 115260
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 66313 0 0 0 12754 217 0 0 25 0 1 0 547253069 118026240 26047 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28815 26047 603 41 0 28774 0
vsize: 115260
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 66405 0 0 0 13754 217 0 0 25 0 1 0 547253069 118439936 26139 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28916 26139 603 41 0 28875 0
vsize: 115664
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 66506 0 0 0 14753 217 0 0 25 0 1 0 547253069 118829056 26240 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29011 26240 603 41 0 28970 0
vsize: 116044
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 67807 0 0 0 15750 221 0 0 25 0 1 0 547253069 126857216 27521 4294967295 134512640 134672761 3221224544 3221222960 134608931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30971 27521 603 41 0 30930 0
vsize: 123884
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 75012 0 0 0 16723 247 0 0 25 0 1 0 547253069 119439360 26394 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29160 26394 603 41 0 29119 0
vsize: 116640
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 75013 0 0 0 17724 247 0 0 25 0 1 0 547253069 119439360 26395 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29160 26395 603 41 0 29119 0
vsize: 116640
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 75013 0 0 0 18724 247 0 0 25 0 1 0 547253069 119439360 26395 4294967295 134512640 134672761 3221224544 3221223680 134614713 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29160 26395 603 41 0 29119 0
vsize: 116640
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 75067 0 0 0 19724 248 0 0 25 0 1 0 547253069 119672832 26449 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29217 26449 603 41 0 29176 0
vsize: 116868
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 75192 0 0 0 20723 248 0 0 25 0 1 0 547253069 120320000 26574 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29375 26574 603 41 0 29334 0
vsize: 117500
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 81687 0 0 0 21701 270 0 0 25 0 1 0 547253069 120864768 26737 4294967295 134512640 134672761 3221224544 3221222064 134522373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29508 26737 603 41 0 29467 0
vsize: 118032
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 83919 0 0 0 22695 276 0 0 25 0 1 0 547253069 120864768 26739 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29508 26739 603 41 0 29467 0
vsize: 118032
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 83919 0 0 0 23695 276 0 0 25 0 1 0 547253069 120864768 26739 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29508 26739 603 41 0 29467 0
vsize: 118032
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 83919 0 0 0 24695 276 0 0 25 0 1 0 547253069 120864768 26739 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29508 26739 603 41 0 29467 0
vsize: 118032
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 83919 0 0 0 25695 276 0 0 25 0 1 0 547253069 120864768 26739 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29508 26739 603 41 0 29467 0
vsize: 118032
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 92081 0 0 0 26669 302 0 0 25 0 1 0 547253069 120950784 26774 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29529 26774 603 41 0 29488 0
vsize: 118116
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 92081 0 0 0 27669 302 0 0 25 0 1 0 547253069 120950784 26774 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29529 26774 603 41 0 29488 0
vsize: 118116
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 92081 0 0 0 28670 302 0 0 25 0 1 0 547253069 120946688 26773 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29528 26773 603 41 0 29487 0
vsize: 118112
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 92118 0 0 0 29670 302 0 0 25 0 1 0 547253069 121155584 26810 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29579 26810 603 41 0 29538 0
vsize: 118316
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 104899 0 0 0 30627 345 0 0 25 0 1 0 547253069 146124800 31700 4294967295 134512640 134672761 3221224544 3221223256 134643250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35675 31700 603 41 0 35634 0
vsize: 142700
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 106279 0 0 0 31623 348 0 0 25 0 1 0 547253069 137887744 30430 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33664 30430 603 41 0 33623 0
vsize: 134656
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 112334 0 0 0 32605 366 0 0 25 0 1 0 547253069 166268928 36329 4294967295 134512640 134672761 3221224544 3221222920 1075384046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40593 36329 603 41 0 40552 0
vsize: 162372
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 115701 0 0 0 33592 378 0 0 25 0 1 0 547253069 138051584 30518 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33704 30518 603 41 0 33663 0
vsize: 134816
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 115727 0 0 0 34592 378 0 0 25 0 1 0 547253069 138051584 30544 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33704 30544 603 41 0 33663 0
vsize: 134816
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 125200 0 0 0 35560 410 0 0 25 0 1 0 547253069 138055680 30561 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33705 30561 603 41 0 33664 0
vsize: 134820
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 125200 0 0 0 36561 410 0 0 25 0 1 0 547253069 138055680 30561 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33705 30561 603 41 0 33664 0
vsize: 134820
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 125200 0 0 0 37561 410 0 0 25 0 1 0 547253069 138055680 30561 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33705 30561 603 41 0 33664 0
vsize: 134820
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 125201 0 0 0 38561 410 0 0 25 0 1 0 547253069 138055680 30562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33705 30562 603 41 0 33664 0
vsize: 134820
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 125201 0 0 0 39561 410 0 0 25 0 1 0 547253069 138055680 30562 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33705 30562 603 41 0 33664 0
vsize: 134820
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 135036 0 0 0 40527 444 0 0 25 0 1 0 547253069 138059776 30588 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 30588 603 41 0 33665 0
vsize: 134824
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 135036 0 0 0 41527 444 0 0 25 0 1 0 547253069 138059776 30588 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 30588 603 41 0 33665 0
vsize: 134824
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 135037 0 0 0 42527 444 0 0 25 0 1 0 547253069 138059776 30589 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 30589 603 41 0 33665 0
vsize: 134824
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 135037 0 0 0 43527 444 0 0 25 0 1 0 547253069 138059776 30589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 30589 603 41 0 33665 0
vsize: 134824
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 152081 0 0 0 44471 500 0 0 25 0 1 0 547253069 169754624 37605 4294967295 134512640 134672761 3221224544 3221222776 1075352388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41444 37605 603 41 0 41403 0
vsize: 165776
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 153358 0 0 0 45467 505 0 0 25 0 1 0 547253069 138129408 30610 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33723 30610 603 41 0 33682 0
vsize: 134892
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 153359 0 0 0 46467 505 0 0 25 0 1 0 547253069 138129408 30611 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33723 30611 603 41 0 33682 0
vsize: 134892
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 153368 0 0 0 47467 505 0 0 25 0 1 0 547253069 138264576 30620 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33756 30620 603 41 0 33715 0
vsize: 135024
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 153411 0 0 0 48467 505 0 0 25 0 1 0 547253069 138391552 30663 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33787 30663 603 41 0 33746 0
vsize: 135148
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 161030 0 0 0 49443 530 0 0 25 0 1 0 547253069 143790080 31968 4294967295 134512640 134672761 3221224544 3221223708 1075349962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35105 31968 603 41 0 35064 0
vsize: 140420
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 162194 0 0 0 50439 533 0 0 25 0 1 0 547253069 143765504 31970 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31970 603 41 0 35058 0
vsize: 140396
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 162195 0 0 0 51438 533 0 0 25 0 1 0 547253069 143765504 31971 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31971 603 41 0 35058 0
vsize: 140396
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 162195 0 0 0 52439 533 0 0 25 0 1 0 547253069 143765504 31971 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31971 603 41 0 35058 0
vsize: 140396
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 170871 0 0 0 53410 560 0 0 25 0 1 0 547253069 143765504 31990 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31990 603 41 0 35058 0
vsize: 140396
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 170871 0 0 0 54410 560 0 0 25 0 1 0 547253069 143765504 31990 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31990 603 41 0 35058 0
vsize: 140396
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 176179 0 0 0 55394 577 0 0 25 0 1 0 547253069 169353216 37298 4294967295 134512640 134672761 3221224544 3221222988 1075278885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41346 37298 603 41 0 41305 0
vsize: 165384
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 178497 0 0 0 56384 586 0 0 25 0 1 0 547253069 143765504 31993 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 178497 0 0 0 57384 586 0 0 25 0 1 0 547253069 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 178497 0 0 0 58385 586 0 0 25 0 1 0 547253069 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 178497 0 0 0 59385 586 0 0 25 0 1 0 547253069 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 178497 0 0 0 60385 586 0 0 25 0 1 0 547253069 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 178497 0 0 0 61385 586 0 0 25 0 1 0 547253069 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 178497 0 0 0 62385 586 0 0 25 0 1 0 547253069 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 178497 0 0 0 63385 586 0 0 25 0 1 0 547253069 143765504 31993 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 183016 0 0 0 64375 597 0 0 25 0 1 0 547253069 168300544 36512 4294967295 134512640 134672761 3221224544 3221222880 134605465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41089 36512 603 41 0 41048 0
vsize: 164356
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186201 0 0 0 65358 614 0 0 25 0 1 0 547253069 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186201 0 0 0 66358 614 0 0 25 0 1 0 547253069 143765504 31994 4294967295 134512640 134672761 3221224544 3221223692 134614482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186201 0 0 0 67358 614 0 0 25 0 1 0 547253069 143765504 31994 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186201 0 0 0 68358 614 0 0 25 0 1 0 547253069 143765504 31994 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186201 0 0 0 69358 614 0 0 25 0 1 0 547253069 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186201 0 0 0 70359 614 0 0 25 0 1 0 547253069 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186201 0 0 0 71359 614 0 0 25 0 1 0 547253069 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186233 0 0 0 72359 614 0 0 25 0 1 0 547253069 143896576 32026 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35131 32026 603 41 0 35090 0
vsize: 140524
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186372 0 0 0 73359 614 0 0 25 0 1 0 547253069 144539648 32165 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35288 32165 603 41 0 35247 0
vsize: 141152
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186494 0 0 0 74359 614 0 0 25 0 1 0 547253069 145063936 32287 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35416 32287 603 41 0 35375 0
vsize: 141664
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186577 0 0 0 75358 615 0 0 25 0 1 0 547253069 145301504 32370 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35474 32370 603 41 0 35433 0
vsize: 141896
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 186804 0 0 0 76358 615 0 0 25 0 1 0 547253069 146337792 32597 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35727 32597 603 41 0 35686 0
vsize: 142908
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 187045 0 0 0 77358 616 0 0 25 0 1 0 547253069 147218432 32838 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35942 32838 603 41 0 35901 0
vsize: 143768
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 187228 0 0 0 78358 616 0 0 25 0 1 0 547253069 148058112 33021 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36147 33021 603 41 0 36106 0
vsize: 144588
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 194585 0 0 0 79333 641 0 0 25 0 1 0 547253069 181633024 40282 4294967295 134512640 134672761 3221224544 3221222628 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44344 40282 603 41 0 44303 0
vsize: 177376
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 196146 0 0 0 80326 647 0 0 25 0 1 0 547253069 148709376 33206 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36306 33206 603 41 0 36265 0
vsize: 145224
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 196390 0 0 0 81326 647 0 0 25 0 1 0 547253069 149692416 33450 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36546 33450 603 41 0 36505 0
vsize: 146184
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 196583 0 0 0 82326 648 0 0 25 0 1 0 547253069 150577152 33643 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36762 33643 603 41 0 36721 0
vsize: 147048
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 196835 0 0 0 83325 649 0 0 25 0 1 0 547253069 151584768 33895 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37008 33895 603 41 0 36967 0
vsize: 148032
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 197024 0 0 0 84325 649 0 0 25 0 1 0 547253069 152346624 34084 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37194 34084 603 41 0 37153 0
vsize: 148776
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 197086 0 0 0 85325 649 0 0 25 0 1 0 547253069 152604672 34146 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37257 34146 603 41 0 37216 0
vsize: 149028
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 197178 0 0 0 86326 650 0 0 25 0 1 0 547253069 152981504 34238 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37349 34238 603 41 0 37308 0
vsize: 149396
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 197179 0 0 0 87326 650 0 0 25 0 1 0 547253069 152981504 34239 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37349 34239 603 41 0 37308 0
vsize: 149396
[startup+890.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 197418 0 0 0 88325 650 0 0 25 0 1 0 547253069 154005504 34478 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37599 34478 603 41 0 37558 0
vsize: 150396
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 197647 0 0 0 89325 651 0 0 25 0 1 0 547253069 154906624 34707 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37819 34707 603 41 0 37778 0
vsize: 151276
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 197912 0 0 0 90325 651 0 0 25 0 1 0 547253069 155934720 34972 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38070 34972 603 41 0 38029 0
vsize: 152280
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198121 0 0 0 91325 652 0 0 25 0 1 0 547253069 156844032 35181 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38292 35181 603 41 0 38251 0
vsize: 153168
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 92325 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+940.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 93325 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 94325 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+960.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 95325 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 96325 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 97325 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 98325 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 99326 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 100326 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223584 134613761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 101326 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 102326 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 103326 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 104327 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 105327 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 106327 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 107327 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 108327 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 109327 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 110328 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 153760
[startup+1115.54 s]
Raw data (loadavg): 0.99 0.97 0.95 1/53 23291
Raw data (stat): 23291 (minisat+) R 23290 11931 11930 0 -1 0 198262 0 0 0 110328 652 0 0 25 0 1 0 547253069 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38440 35322 603 41 0 38399 0
vsize: 0

Child status: 30
Real time (s): 1115.54
CPU time (s): 1115.3
CPU user time (s): 1108.68
CPU system time (s): 6.62299
CPU usage (%): 99.9788
Max. virtual memory (Kb): 177376
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	58880896
#### END VERIFIER DATA ####