PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-egout.opb
MD5SUM	fd101f0ba1a3813e843a38997ab7ed84
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.04984
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 15182

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 03:18:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18302 boxname=wulflinc20 idbench=1408 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fd101f0ba1a3813e843a38997ab7ed84  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-egout.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-egout.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-egout.opb
IDLAUNCH: 18302
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        677232 kB
Buffers:         19840 kB
Cached:         313648 kB
SwapCached:        528 kB
Active:         106540 kB
Inactive:       228976 kB
HighTotal:      131008 kB
HighFree:          644 kB
LowTotal:       903652 kB
LowFree:        676588 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            16428 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:36:35 (client local time) WITH STATUS 30 IN 1111.24 SECONDS
stats: 18302 0 1111.24 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.485926 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.0351 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.2253 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: 57.9592 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.5861 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.4289 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.74 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: 215.023 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.777 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: 298.384 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: 325.091 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.767 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: 397.031 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.674 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.7 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: 492.045 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: 527.384 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.595 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.658 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.009 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      (249019 /sec)
c inspects              : 1029485597     (932317 /sec)
c CPU time              : 1104.22 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.93 0.98 0.92 2/54 28090
Raw data (stat): 28090 (runsolver) R 28089 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541777663 1052672 99 4294967295 134512640 135381576 3221224448 3221219700 134863748 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 14548 0 0 0 953 45 0 0 25 0 1 0 541777663 66039808 13724 4294967295 134512640 134672761 3221224544 3221222752 1075730206 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.0016 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 18131 0 0 0 1940 57 0 0 25 0 1 0 541777663 79880192 16273 4294967295 134512640 134672761 3221224544 3221222920 1075384026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19502 16273 603 41 0 19461 0
vsize: 78008
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 26448 0 0 0 2910 87 0 0 25 0 1 0 541777663 102182912 20530 4294967295 134512640 134672761 3221224544 3221223036 134642887 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.0024 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 27370 0 0 0 3907 90 0 0 25 0 1 0 541777663 96030720 19548 4294967295 134512640 134672761 3221224544 3221223728 134615581 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.0029 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 39553 0 0 0 4872 125 0 0 25 0 1 0 541777663 124465152 27042 4294967295 134512640 134672761 3221224544 3221223088 134621104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30387 27042 603 41 0 30346 0
vsize: 121548
[startup+60.0037 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 47411 0 0 0 5840 156 0 0 25 0 1 0 541777663 144035840 30692 4294967295 134512640 134672761 3221224544 3221222988 1075278863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35165 30692 603 41 0 35124 0
vsize: 140660
[startup+70.0048 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 49447 0 0 0 6827 169 0 0 25 0 1 0 541777663 117383168 25828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28658 25828 603 41 0 28617 0
vsize: 114632
[startup+80.0089 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 49476 0 0 0 7827 169 0 0 25 0 1 0 541777663 117510144 25857 4294967295 134512640 134672761 3221224544 3221223744 134610661 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.0089 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 49500 0 0 0 8827 169 0 0 25 0 1 0 541777663 117645312 25881 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28722 25881 603 41 0 28681 0
vsize: 114888
[startup+100.009 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 57804 0 0 0 9799 197 0 0 25 0 1 0 541777663 117723136 25958 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 66254 0 0 0 10770 226 0 0 25 0 1 0 541777663 117772288 25988 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 66295 0 0 0 11770 226 0 0 25 0 1 0 541777663 118026240 26029 4294967295 134512640 134672761 3221224544 3221223728 134615663 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.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 66313 0 0 0 12770 227 0 0 25 0 1 0 541777663 118026240 26047 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 66405 0 0 0 13770 227 0 0 25 0 1 0 541777663 118439936 26139 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28916 26139 603 41 0 28875 0
vsize: 115664
[startup+150.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 66504 0 0 0 14769 227 0 0 25 0 1 0 541777663 118829056 26238 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29011 26238 603 41 0 28970 0
vsize: 116044
[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 66626 0 0 0 15769 228 0 0 25 0 1 0 541777663 119349248 26360 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29138 26360 603 41 0 29097 0
vsize: 116552
[startup+170.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 75012 0 0 0 16742 255 0 0 25 0 1 0 541777663 119439360 26394 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29160 26394 603 41 0 29119 0
vsize: 116640
[startup+180.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 75013 0 0 0 17742 255 0 0 25 0 1 0 541777663 119439360 26395 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29160 26395 603 41 0 29119 0
vsize: 116640
[startup+190.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 75013 0 0 0 18742 255 0 0 25 0 1 0 541777663 119439360 26395 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29160 26395 603 41 0 29119 0
vsize: 116640
[startup+200.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 75067 0 0 0 19741 256 0 0 25 0 1 0 541777663 119672832 26449 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 75174 0 0 0 20741 257 0 0 25 0 1 0 541777663 120188928 26556 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29343 26556 603 41 0 29302 0
vsize: 117372
[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 81667 0 0 0 21718 280 0 0 25 0 1 0 541777663 136208384 29780 4294967295 134512640 134672761 3221224544 3221222912 134553654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33254 29780 603 41 0 33213 0
vsize: 133016
[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 83919 0 0 0 22711 287 0 0 25 0 1 0 541777663 120864768 26739 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29508 26739 603 41 0 29467 0
vsize: 118032
[startup+240.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 83919 0 0 0 23710 287 0 0 25 0 1 0 541777663 120864768 26739 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29508 26739 603 41 0 29467 0
vsize: 118032
[startup+250.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 83919 0 0 0 24710 287 0 0 25 0 1 0 541777663 120864768 26739 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29508 26739 603 41 0 29467 0
vsize: 118032
[startup+260.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 83919 0 0 0 25710 288 0 0 25 0 1 0 541777663 120864768 26739 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29508 26739 603 41 0 29467 0
vsize: 118032
[startup+270.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 92081 0 0 0 26685 312 0 0 25 0 1 0 541777663 120950784 26774 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29529 26774 603 41 0 29488 0
vsize: 118116
[startup+280.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 92081 0 0 0 27685 313 0 0 25 0 1 0 541777663 120950784 26774 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29529 26774 603 41 0 29488 0
vsize: 118116
[startup+290.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 92081 0 0 0 28685 313 0 0 25 0 1 0 541777663 120946688 26773 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29528 26773 603 41 0 29487 0
vsize: 118112
[startup+300.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 92116 0 0 0 29684 314 0 0 25 0 1 0 541777663 121155584 26808 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29579 26808 603 41 0 29538 0
vsize: 118316
[startup+310.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 103620 0 0 0 30640 354 0 0 25 0 1 0 541777663 138280960 30459 4294967295 134512640 134672761 3221224544 3221222992 134643483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33760 30459 603 41 0 33719 0
vsize: 135040
[startup+320.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 106279 0 0 0 31633 361 0 0 25 0 1 0 541777663 137887744 30430 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33664 30430 603 41 0 33623 0
vsize: 134656
[startup+330.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 112300 0 0 0 32616 378 0 0 25 0 1 0 541777663 166268928 36295 4294967295 134512640 134672761 3221224544 3221222880 134603709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40593 36295 603 41 0 40552 0
vsize: 162372
[startup+340.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 115701 0 0 0 33603 392 0 0 25 0 1 0 541777663 138051584 30518 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33704 30518 603 41 0 33663 0
vsize: 134816
[startup+350.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 115727 0 0 0 34602 392 0 0 25 0 1 0 541777663 138051584 30544 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33704 30544 603 41 0 33663 0
vsize: 134816
[startup+360.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 125200 0 0 0 35570 425 0 0 25 0 1 0 541777663 138055680 30561 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33705 30561 603 41 0 33664 0
vsize: 134820
[startup+370.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 125200 0 0 0 36570 425 0 0 25 0 1 0 541777663 138055680 30561 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33705 30561 603 41 0 33664 0
vsize: 134820
[startup+380.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 125200 0 0 0 37570 425 0 0 25 0 1 0 541777663 138055680 30561 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33705 30561 603 41 0 33664 0
vsize: 134820
[startup+390.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 125201 0 0 0 38570 426 0 0 25 0 1 0 541777663 138055680 30562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33705 30562 603 41 0 33664 0
vsize: 134820
[startup+400.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 125201 0 0 0 39570 426 0 0 25 0 1 0 541777663 138055680 30562 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33705 30562 603 41 0 33664 0
vsize: 134820
[startup+410.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 135036 0 0 0 40535 461 0 0 25 0 1 0 541777663 138059776 30588 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 135036 0 0 0 41534 461 0 0 25 0 1 0 541777663 138059776 30588 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 30588 603 41 0 33665 0
vsize: 134824
[startup+430.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 135037 0 0 0 42535 461 0 0 25 0 1 0 541777663 138059776 30589 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 30589 603 41 0 33665 0
vsize: 134824
[startup+440.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 135037 0 0 0 43535 461 0 0 25 0 1 0 541777663 138059776 30589 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 30589 603 41 0 33665 0
vsize: 134824
[startup+450.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 151664 0 0 0 44479 517 0 0 25 0 1 0 541777663 170151936 37417 4294967295 134512640 134672761 3221224544 3221222880 134605751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41541 37417 603 41 0 41500 0
vsize: 166164
[startup+460.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 153358 0 0 0 45472 524 0 0 25 0 1 0 541777663 138129408 30610 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33723 30610 603 41 0 33682 0
vsize: 134892
[startup+470.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 153359 0 0 0 46472 524 0 0 25 0 1 0 541777663 138129408 30611 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33723 30611 603 41 0 33682 0
vsize: 134892
[startup+480.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 153366 0 0 0 47472 525 0 0 25 0 1 0 541777663 138264576 30618 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33756 30618 603 41 0 33715 0
vsize: 135024
[startup+490.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 153411 0 0 0 48472 525 0 0 25 0 1 0 541777663 138391552 30663 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33787 30663 603 41 0 33746 0
vsize: 135148
[startup+500.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 161030 0 0 0 49445 551 0 0 25 0 1 0 541777663 170844160 37850 4294967295 134512640 134672761 3221224544 3221222992 134611682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41710 37850 603 41 0 41669 0
vsize: 166840
[startup+510.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 162194 0 0 0 50442 555 0 0 25 0 1 0 541777663 143765504 31970 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 162195 0 0 0 51442 555 0 0 25 0 1 0 541777663 143765504 31971 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31971 603 41 0 35058 0
vsize: 140396
[startup+530.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 162195 0 0 0 52442 555 0 0 25 0 1 0 541777663 143765504 31971 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31971 603 41 0 35058 0
vsize: 140396
[startup+540.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 170871 0 0 0 53413 584 0 0 25 0 1 0 541777663 143765504 31990 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 170871 0 0 0 54413 584 0 0 25 0 1 0 541777663 143765504 31990 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31990 603 41 0 35058 0
vsize: 140396
[startup+560.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 176133 0 0 0 55400 598 0 0 25 0 1 0 541777663 169353216 37252 4294967295 134512640 134672761 3221224544 3221222848 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41346 37252 603 41 0 41305 0
vsize: 165384
[startup+570.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 178497 0 0 0 56389 608 0 0 25 0 1 0 541777663 143765504 31993 4294967295 134512640 134672761 3221224544 3221223536 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+580.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 178497 0 0 0 57389 609 0 0 25 0 1 0 541777663 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+590.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 178497 0 0 0 58388 609 0 0 25 0 1 0 541777663 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+600.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 178497 0 0 0 59388 610 0 0 25 0 1 0 541777663 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+610.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 178497 0 0 0 60388 610 0 0 25 0 1 0 541777663 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+620.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 178497 0 0 0 61388 610 0 0 25 0 1 0 541777663 143765504 31993 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+630.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 178497 0 0 0 62388 610 0 0 25 0 1 0 541777663 143765504 31993 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+640.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 178497 0 0 0 63388 610 0 0 25 0 1 0 541777663 143765504 31993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31993 603 41 0 35058 0
vsize: 140396
[startup+650.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 180129 0 0 0 64384 614 0 0 25 0 1 0 541777663 155455488 33625 4294967295 134512640 134672761 3221224544 3221222960 134609557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37953 33625 603 41 0 37912 0
vsize: 151812
[startup+660.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186201 0 0 0 65359 640 0 0 25 0 1 0 541777663 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+670.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186201 0 0 0 66359 640 0 0 25 0 1 0 541777663 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+680.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186201 0 0 0 67359 640 0 0 25 0 1 0 541777663 143765504 31994 4294967295 134512640 134672761 3221224544 3221223536 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+690.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186201 0 0 0 68359 641 0 0 25 0 1 0 541777663 143765504 31994 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+700.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186201 0 0 0 69359 641 0 0 25 0 1 0 541777663 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+710.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186201 0 0 0 70359 641 0 0 25 0 1 0 541777663 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+720.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186201 0 0 0 71358 641 0 0 25 0 1 0 541777663 143765504 31994 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35099 31994 603 41 0 35058 0
vsize: 140396
[startup+730.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186225 0 0 0 72358 642 0 0 25 0 1 0 541777663 143896576 32018 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35131 32018 603 41 0 35090 0
vsize: 140524
[startup+740.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186372 0 0 0 73358 642 0 0 25 0 1 0 541777663 144539648 32165 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35288 32165 603 41 0 35247 0
vsize: 141152
[startup+750.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186492 0 0 0 74358 642 0 0 25 0 1 0 541777663 145063936 32285 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35416 32285 603 41 0 35375 0
vsize: 141664
[startup+760.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186573 0 0 0 75357 643 0 0 25 0 1 0 541777663 145301504 32366 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35474 32366 603 41 0 35433 0
vsize: 141896
[startup+770.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 186796 0 0 0 76356 644 0 0 25 0 1 0 541777663 146190336 32589 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35691 32589 603 41 0 35650 0
vsize: 142764
[startup+780.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 187045 0 0 0 77356 645 0 0 25 0 1 0 541777663 147218432 32838 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35942 32838 603 41 0 35901 0
vsize: 143768
[startup+790.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 187228 0 0 0 78355 646 0 0 25 0 1 0 541777663 148058112 33021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36147 33021 603 41 0 36106 0
vsize: 144588
[startup+800.039 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 194549 0 0 0 79329 671 0 0 25 0 1 0 541777663 181497856 40246 4294967295 134512640 134672761 3221224544 3221222736 134615576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44311 40246 603 41 0 44270 0
vsize: 177244
[startup+810.041 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 196141 0 0 0 80324 677 0 0 25 0 1 0 541777663 148709376 33201 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36306 33201 603 41 0 36265 0
vsize: 145224
[startup+820.041 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 196390 0 0 0 81323 678 0 0 25 0 1 0 541777663 149692416 33450 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.04 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 196585 0 0 0 82322 679 0 0 25 0 1 0 541777663 150577152 33645 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36762 33645 603 41 0 36721 0
vsize: 147048
[startup+840.041 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 196859 0 0 0 83322 679 0 0 25 0 1 0 541777663 151691264 33919 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37034 33919 603 41 0 36993 0
vsize: 148136
[startup+850.041 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 197024 0 0 0 84322 679 0 0 25 0 1 0 541777663 152346624 34084 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.042 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 197086 0 0 0 85322 680 0 0 25 0 1 0 541777663 152604672 34146 4294967295 134512640 134672761 3221224544 3221223728 134617709 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.042 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 197179 0 0 0 86321 680 0 0 25 0 1 0 541777663 152981504 34239 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37349 34239 603 41 0 37308 0
vsize: 149396
[startup+880.042 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 197202 0 0 0 87322 680 0 0 25 0 1 0 541777663 153108480 34262 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37380 34262 603 41 0 37339 0
vsize: 149520
[startup+890.043 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 197437 0 0 0 88321 681 0 0 25 0 1 0 541777663 154005504 34497 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37599 34497 603 41 0 37558 0
vsize: 150396
[startup+900.042 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 197667 0 0 0 89320 682 0 0 25 0 1 0 541777663 155041792 34727 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37852 34727 603 41 0 37811 0
vsize: 151408
[startup+910.043 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 197957 0 0 0 90320 682 0 0 25 0 1 0 541777663 156196864 35017 4294967295 134512640 134672761 3221224544 3221223680 134614516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38134 35017 603 41 0 38093 0
vsize: 152536
[startup+920.043 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198153 0 0 0 91320 683 0 0 25 0 1 0 541777663 156971008 35213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38323 35213 603 41 0 38282 0
vsize: 153292
[startup+930.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 92320 683 0 0 25 0 1 0 541777663 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+940.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 93320 683 0 0 25 0 1 0 541777663 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+950.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 94320 683 0 0 25 0 1 0 541777663 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.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 95320 683 0 0 25 0 1 0 541777663 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+970.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 96321 683 0 0 25 0 1 0 541777663 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.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 97321 683 0 0 25 0 1 0 541777663 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+990.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 98321 683 0 0 25 0 1 0 541777663 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615560 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.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 99321 683 0 0 25 0 1 0 541777663 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+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 100321 683 0 0 25 0 1 0 541777663 157450240 35322 4294967295 134512640 134672761 3221224544 3221223680 134614753 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.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 101322 683 0 0 25 0 1 0 541777663 157450240 35322 4294967295 134512640 134672761 3221224544 3221223584 134612987 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.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 102322 683 0 0 25 0 1 0 541777663 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 103322 683 0 0 25 0 1 0 541777663 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+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 104322 683 0 0 25 0 1 0 541777663 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+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 105322 683 0 0 25 0 1 0 541777663 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.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 106323 683 0 0 25 0 1 0 541777663 157450240 35322 4294967295 134512640 134672761 3221224544 3221223680 134614690 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.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 107323 683 0 0 25 0 1 0 541777663 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+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 108323 683 0 0 25 0 1 0 541777663 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+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198262 0 0 0 109323 683 0 0 25 0 1 0 541777663 157450240 35322 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198376 0 0 0 110323 684 0 0 25 0 1 0 541777663 157974528 35436 4294967295 134512640 134672761 3221224544 3221223568 134606928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38568 35436 603 41 0 38527 0
vsize: 154272
[startup+1111.22 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 28090
Raw data (stat): 28090 (minisat+) R 28089 27565 27564 0 -1 0 198376 0 0 0 110323 684 0 0 25 0 1 0 541777663 157974528 35436 4294967295 134512640 134672761 3221224544 3221223568 134606928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38568 35436 603 41 0 38527 0
vsize: 0

Child status: 30
Real time (s): 1111.22
CPU time (s): 1111.24
CPU user time (s): 1104.31
CPU system time (s): 6.93195
CPU usage (%): 100.002
Max. virtual memory (Kb): 177244
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	58880896
#### END VERIFIER DATA ####