PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-sample2.opb
MD5SUM	d28092793cdc5a919be9a0f5974c70fe
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	48000
Optimality of the best value was proved	NO
Number of terms in the objective function	489
Biggest coefficient in the objective function	3145728
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	69282750
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	3145728
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	69282750
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	10.6134
Number of variables	873
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	43
Minimum length of a constraint	1
Maximum length of a constraint	100
Trace number 18879

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 17:17:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17249 boxname=wulflinc7 idbench=1327 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d28092793cdc5a919be9a0f5974c70fe  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sample2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sample2.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sample2.opb
IDLAUNCH: 17249
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        767668 kB
Buffers:         11880 kB
Cached:         233636 kB
SwapCached:        304 kB
Active:          19412 kB
Inactive:       228684 kB
HighTotal:      131008 kB
HighFree:        68712 kB
LowTotal:       903652 kB
LowFree:        698956 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6448 kB
Slab:            13124 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:18:23 (client local time) WITH STATUS 30 IN 54.8577 SECONDS
stats: 17249 0 54.8577 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 67 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #####################
c   -- Clauses(.)/Splits(s): (none)
c ---[  66]---> BDD-cost:   11
c ---[  64]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  422     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> Sorter-cost:  422     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  422     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  422     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> BDD-cost:    5
c ---[  34]---> BDD-cost:    5
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:   19
c ---[  31]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   17
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:   17
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   17
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   19
c ---[  10]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  716     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  716     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  716     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   25401    59714 |    7620       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8335          
c   -- var.elim.:  2000/8335          
c   -- var.elim.:  3000/8335          
c   -- var.elim.:  4000/8335          
c   -- var.elim.:  5000/8335          
c   -- var.elim.:  6000/8335          
c   -- var.elim.:  7000/8335          
c   -- var.elim.:  8000/8335          
c   -- var.elim.:  8335/8335          
c   -- var.elim.:  1000/4566          
c   -- var.elim.:  2000/4566          
c   -- var.elim.:  3000/4566          
c   -- var.elim.:  4000/4566          
c   -- var.elim.:  4566/4566          
c   -- var.elim.:  499/499          
c   -- var.elim.:  176/176          
c   -- subsuming                       
c   -- var.elim.:  1000/2011          
c   -- var.elim.:  2000/2011          
c   -- var.elim.:  2011/2011          
c   -- var.elim.:  1000/1167          
c   -- var.elim.:  1167/1167          
c   -- var.elim.:  15/15          
c   -- subsuming                       
c   -- var.elim.:  173/173          
c   -- var.elim.:  19/19          
c |         0 |   19319    55898 |      --       0       --      -- |     --   | -4554/59
c |         0 |   19319    55898 |    7727       0        0     nan |  0.000 % |
c |       102 |   19098    55134 |    8403      73      297     4.1 | 20.179 % |
c ==============================================================================
c (current CPU-time: 1.42178 s)
c ==============================================================================
c [1mFound solution: 104532[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:15204     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       118 |   57931   145733 |   17379      87      378     4.3 | 20.179 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14323          
c   -- var.elim.:  2000/14323          
c   -- var.elim.:  3000/14323          
c   -- var.elim.:  4000/14323          
c   -- var.elim.:  5000/14323          
c   -- var.elim.:  6000/14323          
c   -- var.elim.:  7000/14323          
c   -- var.elim.:  8000/14323          
c   -- var.elim.:  9000/14323          
c   -- var.elim.:  10000/14323          
c   -- var.elim.:  11000/14323          
c   -- var.elim.:  12000/14323          
c   -- var.elim.:  13000/14323          
c   -- var.elim.:  14000/14323          
c   -- var.elim.:  14323/14323          
c   -- var.elim.:  1000/7992          
c   -- var.elim.:  2000/7992          
c   -- var.elim.:  3000/7992          
c   -- var.elim.:  4000/7992          
c   -- var.elim.:  5000/7992          
c   -- var.elim.:  6000/7992          
c   -- var.elim.:  7000/7992          
c   -- var.elim.:  7992/7992          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  865/865          
c   -- var.elim.:  135/135          
c   -- subsuming                       
c   -- var.elim.:  181/181          
c   -- var.elim.:  135/135          
c |       118 |   53748   163351 |      --      87       --      -- |     --   | -4172/17645
c |       118 |   53748   163351 |   21499      78      343     4.4 | 20.179 % |
c |       219 |   53563   162464 |   23567     175     1385     7.9 |  8.735 % |
c |       369 |   53563   162464 |   25924     325     2697     8.3 |  8.735 % |
c |       594 |   53396   161698 |   28428     544     3955     7.3 |  8.874 % |
c |       931 |   52667   158827 |   30843     843    12344    14.6 |  9.652 % |
c |      1438 |   52332   157712 |   33712    1342    17990    13.4 | 10.037 % |
c ==============================================================================
c (current CPU-time: 5.31819 s)
c ==============================================================================
c [1mFound solution: 103364[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:10108     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1781 |   77713   216379 |   23313    1648    20487    12.4 | 10.037 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11897          
c   -- var.elim.:  2000/11897          
c   -- var.elim.:  3000/11897          
c   -- var.elim.:  4000/11897          
c   -- var.elim.:  5000/11897          
c   -- var.elim.:  6000/11897          
c   -- var.elim.:  7000/11897          
c   -- var.elim.:  8000/11897          
c   -- var.elim.:  9000/11897          
c   -- var.elim.:  10000/11897          
c   -- var.elim.:  11000/11897          
c   -- var.elim.:  11897/11897          
c   -- var.elim.:  1000/6944          
c   -- var.elim.:  2000/6944          
c   -- var.elim.:  3000/6944          
c   -- var.elim.:  4000/6944          
c   -- var.elim.:  5000/6944          
c   -- var.elim.:  6000/6944          
c   -- var.elim.:  6944/6944          
c   -- var.elim.:  528/528          
c   -- var.elim.:  263/263          
c   -- subsuming                       
c   -- var.elim.:  1000/1000          
c   -- var.elim.:  102/102          
c |      1781 |   73109   223792 |      --    1648       --      -- |     --   | -4346/8035
c |      1781 |   73109   223792 |   29243    1480    14728    10.0 | 10.037 % |
c |      1882 |   73109   223792 |   32167    1581    18077    11.4 |  8.840 % |
c |      2033 |   73109   223792 |   35384    1732    19892    11.5 |  8.840 % |
c ==============================================================================
c (current CPU-time: 8.31973 s)
c ==============================================================================
c [1mFound solution: 101788[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 9523     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2159 |   96560   278013 |   28967    1773    20867    11.8 |  8.840 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10133          
c   -- var.elim.:  2000/10133          
c   -- var.elim.:  3000/10133          
c   -- var.elim.:  4000/10133          
c   -- var.elim.:  5000/10133          
c   -- var.elim.:  6000/10133          
c   -- var.elim.:  7000/10133          
c   -- var.elim.:  8000/10133          
c   -- var.elim.:  9000/10133          
c   -- var.elim.:  10000/10133          
c   -- var.elim.:  10133/10133          
c   -- var.elim.:  1000/5687          
c   -- var.elim.:  2000/5687          
c   -- var.elim.:  3000/5687          
c   -- var.elim.:  4000/5687          
c   -- var.elim.:  5000/5687          
c   -- var.elim.:  5687/5687          
c   -- var.elim.:  352/352          
c   -- var.elim.:  98/98          
c   -- subsuming                       
c   -- var.elim.:  913/913          
c   -- var.elim.:  75/75          
c |      2159 |   92608   285281 |      --    1773       --      -- |     --   | -3664/7966
c |      2159 |   92608   285281 |   37043    1733    19871    11.5 |  8.840 % |
c |      2259 |   92190   283825 |   40563    1800    20807    11.6 |  8.387 % |
c |      2409 |   91215   280071 |   44148    1929    22563    11.7 |  8.865 % |
c |      2635 |   89897   275344 |   47861    2145    25261    11.8 |  9.652 % |
c ==============================================================================
c (current CPU-time: 11.6992 s)
c ==============================================================================
c [1mFound solution: 84566[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 9784     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2789 |  111666   323570 |   33499    2262    26560    11.7 |  9.652 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12471          
c   -- var.elim.:  2000/12471          
c   -- var.elim.:  3000/12471          
c   -- var.elim.:  4000/12471          
c   -- var.elim.:  5000/12471          
c   -- var.elim.:  6000/12471          
c   -- var.elim.:  7000/12471          
c   -- var.elim.:  8000/12471          
c   -- var.elim.:  9000/12471          
c   -- var.elim.:  10000/12471          
c   -- var.elim.:  11000/12471          
c   -- var.elim.:  12000/12471          
c   -- var.elim.:  12471/12471          
c   -- var.elim.:  1000/7405          
c   -- var.elim.:  2000/7405          
c   -- var.elim.:  3000/7405          
c   -- var.elim.:  4000/7405          
c   -- var.elim.:  5000/7405          
c   -- var.elim.:  6000/7405          
c   -- var.elim.:  7000/7405          
c   -- var.elim.:  7405/7405          
c   -- var.elim.:  207/207          
c   -- var.elim.:  230/230          
c   -- var.elim.:  17/17          
c   -- subsuming                       
c   -- var.elim.:  983/983          
c   -- var.elim.:  279/279          
c   -- subsuming                       
c   -- var.elim.:  221/221          
c   -- var.elim.:  69/69          
c |      2789 |  107333   331753 |      --    2262       --      -- |     --   | -4230/8432
c |      2789 |  107333   331753 |   42933    2067    22270    10.8 |  9.652 % |
c |      2889 |  107153   331109 |   47147    2140    22712    10.6 | 10.309 % |
c |      3039 |  106788   329512 |   51685    2273    26363    11.6 | 10.470 % |
c ==============================================================================
c (current CPU-time: 15.5036 s)
c ==============================================================================
c [1mFound solution: 81236[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 7435     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3059 |  125180   372568 |   37553    2287    26826    11.7 | 10.470 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8182          
c   -- var.elim.:  2000/8182          
c   -- var.elim.:  3000/8182          
c   -- var.elim.:  4000/8182          
c   -- var.elim.:  5000/8182          
c   -- var.elim.:  6000/8182          
c   -- var.elim.:  7000/8182          
c   -- var.elim.:  8000/8182          
c   -- var.elim.:  8182/8182          
c   -- var.elim.:  1000/4685          
c   -- var.elim.:  2000/4685          
c   -- var.elim.:  3000/4685          
c   -- var.elim.:  4000/4685          
c   -- var.elim.:  4685/4685          
c   -- var.elim.:  222/222          
c   -- var.elim.:  204/204          
c   -- subsuming                       
c   -- var.elim.:  683/683          
c   -- var.elim.:  158/158          
c   -- var.elim.:  15/15          
c |      3059 |  122253   379937 |      --    2287       --      -- |     --   | -2858/7535
c |      3059 |  122253   379937 |   48901    2202    25365    11.5 | 10.470 % |
c |      3159 |  122232   379860 |   53782    2301    26898    11.7 |  9.516 % |
c |      3310 |  116610   360366 |   56439    2448    30596    12.5 | 12.070 % |
c |      3536 |  115222   354915 |   61344    2622    33841    12.9 | 12.655 % |
c |      3874 |  114635   352415 |   67134    2956    38400    13.0 | 12.887 % |
c ==============================================================================
c (current CPU-time: 20.7948 s)
c ==============================================================================
c [1mFound solution: 59232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 9937     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4236 |  136235   398490 |   40870    3270    51203    15.7 | 12.887 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15193          
c   -- var.elim.:  2000/15193          
c   -- var.elim.:  3000/15193          
c   -- var.elim.:  4000/15193          
c   -- var.elim.:  5000/15193          
c   -- var.elim.:  6000/15193          
c   -- var.elim.:  7000/15193          
c   -- var.elim.:  8000/15193          
c   -- var.elim.:  9000/15193          
c   -- var.elim.:  10000/15193          
c   -- var.elim.:  11000/15193          
c   -- var.elim.:  12000/15193          
c   -- var.elim.:  13000/15193          
c   -- var.elim.:  14000/15193          
c   -- var.elim.:  15000/15193          
c   -- var.elim.:  15193/15193          
c   -- var.elim.:  1000/10008          
c   -- var.elim.:  2000/10008          
c   -- var.elim.:  3000/10008          
c   -- var.elim.:  4000/10008          
c   -- var.elim.:  5000/10008          
c   -- var.elim.:  6000/10008          
c   -- var.elim.:  7000/10008          
c   -- var.elim.:  8000/10008          
c   -- var.elim.:  9000/10008          
c   -- var.elim.:  10000/10008          
c   -- var.elim.:  10008/10008          
c   -- var.elim.:  1000/1174          
c   -- var.elim.:  1174/1174          
c   -- var.elim.:  1000/1012          
c   -- var.elim.:  1012/1012          
c   -- var.elim.:  14/14          
c   -- var.elim.:  21/21          
c   -- var.elim.:  13/13          
c   -- subsuming                       
c   -- var.elim.:  1000/2104          
c   -- var.elim.:  2000/2104          
c   -- var.elim.:  2104/2104          
c   -- var.elim.:  998/998          
c   -- subsuming                       
c   -- var.elim.:  437/437          
c   -- var.elim.:  25/25          
c |      4236 |  130758   407067 |      --    3270       --      -- |     --   | -5204/9232
c |      4236 |  130758   407067 |   52303    2867    30749    10.7 | 12.887 % |
c |      4336 |  126425   391899 |   55627    2908    32010    11.0 | 14.731 % |
c |      4486 |  126389   391777 |   61172    3056    42204    13.8 | 14.743 % |
c |      4712 |  126294   391429 |   67238    3276    55978    17.1 | 14.785 % |
c ==============================================================================
c (current CPU-time: 28.7666 s)
c ==============================================================================
c [1mFound solution: 57600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 8034     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4803 |  145435   435240 |   43630    3350    58667    17.5 | 14.785 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11246          
c   -- var.elim.:  2000/11246          
c   -- var.elim.:  3000/11246          
c   -- var.elim.:  4000/11246          
c   -- var.elim.:  5000/11246          
c   -- var.elim.:  6000/11246          
c   -- var.elim.:  7000/11246          
c   -- var.elim.:  8000/11246          
c   -- var.elim.:  9000/11246          
c   -- var.elim.:  10000/11246          
c   -- var.elim.:  11000/11246          
c   -- var.elim.:  11246/11246          
c   -- var.elim.:  1000/6709          
c   -- var.elim.:  2000/6709          
c   -- var.elim.:  3000/6709          
c   -- var.elim.:  4000/6709          
c   -- var.elim.:  5000/6709          
c   -- var.elim.:  6000/6709          
c   -- var.elim.:  6709/6709          
c   -- var.elim.:  228/228          
c   -- var.elim.:  150/150          
c   -- subsuming                       
c   -- var.elim.:  1000/1113          
c   -- var.elim.:  1113/1113          
c   -- var.elim.:  177/177          
c   -- subsuming                       
c   -- var.elim.:  120/120          
c   -- var.elim.:  23/23          
c |      4803 |  141390   440277 |      --    3350       --      -- |     --   | -3790/5635
c |      4803 |  141390   440277 |   56556    2951    32701    11.1 | 14.785 % |
c ==============================================================================
c (current CPU-time: 32.2381 s)
c ==============================================================================
c [1mFound solution: 49920[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4892 |  141708   440656 |   42512    3024    37612    12.4 | 14.785 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1078          
c   -- var.elim.:  1078/1078          
c   -- var.elim.:  542/542          
c   -- subsuming                       
c   -- var.elim.:  148/148          
c   -- var.elim.:  13/13          
c |      4892 |  141410   440450 |      --    3024       --      -- |     --   | -291/-191
c |      4892 |  141410   440450 |   56564    2994    36550    12.2 | 14.785 % |
c |      4993 |  141328   439745 |   62184    3079    37215    12.1 | 14.519 % |
c |      5146 |  140952   438271 |   68220    3223    50433    15.6 | 14.728 % |
c |      5372 |  140294   435625 |   74692    3443    70129    20.4 | 14.919 % |
c ==============================================================================
c (current CPU-time: 40.3789 s)
c ==============================================================================
c [1mFound solution: 48000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 7612     Base: 2 2 2 2 2 2 2 2 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5611 |  157940   475761 |   47381    3670    94939    25.9 | 14.919 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10266          
c   -- var.elim.:  2000/10266          
c   -- var.elim.:  3000/10266          
c   -- var.elim.:  4000/10266          
c   -- var.elim.:  5000/10266          
c   -- var.elim.:  6000/10266          
c   -- var.elim.:  7000/10266          
c   -- var.elim.:  8000/10266          
c   -- var.elim.:  9000/10266          
c   -- var.elim.:  10000/10266          
c   -- var.elim.:  10266/10266          
c   -- var.elim.:  1000/5490          
c   -- var.elim.:  2000/5490          
c   -- var.elim.:  3000/5490          
c   -- var.elim.:  4000/5490          
c   -- var.elim.:  5000/5490          
c   -- var.elim.:  5490/5490          
c   -- var.elim.:  305/305          
c   -- var.elim.:  158/158          
c   -- subsuming                       
c   -- var.elim.:  759/759          
c   -- var.elim.:  355/355          
c   -- var.elim.:  46/46          
c   -- subsuming                       
c   -- var.elim.:  22/22          
c |      5611 |  154737   481890 |      --    3670       --      -- |     --   | -2942/6739
c |      5611 |  154737   481890 |   61894    3314    42345    12.8 | 14.919 % |
c |      5711 |  154737   481890 |   68084    3414    53095    15.6 | 14.470 % |
c |      5861 |  154737   481890 |   74892    3564    87088    24.4 | 14.470 % |
c |      6089 |  154715   481714 |   82370    3785   117151    31.0 | 14.497 % |
c |      6426 |  154448   480711 |   90450    4112   162662    39.6 | 14.573 % |
c ==============================================================================
c [1mOptimal solution: 48000[0m
s OPTIMUM FOUND
v -I_0x2e__0x2e__0x2e__0x2e_F01_bit0 -I_0x2e__0x2e__0x2e__0x2e_F02_bit0 I_0x2e__0x2e__0x2e__0x2e_F03_bit0 -I_0x2e_W01W01_bit0 I_0x2e_W02W02_bit0 -I_0x2e_W03W03_bit0 -I_0x2e_D01D01_bit0 I_0x2e_D02D02_bit0 I_0x2e_D03D03_bit0 -F_0x2e_F01W01_bit_7 -F_0x2e_F01W01_bit_6 -F_0x2e_F01W01_bit_5 -F_0x2e_F01W01_bit_4 -F_0x2e_F01W01_bit_3 -F_0x2e_F01W01_bit_2 -F_0x2e_F01W01_bit_1 -F_0x2e_F01W01_bit0 -F_0x2e_F01W01_bit1 -F_0x2e_F01W01_bit2 -F_0x2e_F01W01_bit3 -F_0x2e_F01W01_bit4 -F_0x2e_F01W01_bit5 -F_0x2e_F01W01_bit6 -F_0x2e_F01W01_bit7 -F_0x2e_F01W01_bit8 -F_0x2e_F01W01_bit9 -F_0x2e_F01W01_bit10 -F_0x2e_F01W01_bit11 -F_0x2e_F01W01_bit12 -F_0x2e_F01W02_bit_7 -F_0x2e_F01W02_bit_6 -F_0x2e_F01W02_bit_5 -F_0x2e_F01W02_bit_4 -F_0x2e_F01W02_bit_3 -F_0x2e_F01W02_bit_2 -F_0x2e_F01W02_bit_1 -F_0x2e_F01W02_bit0 -F_0x2e_F01W02_bit1 -F_0x2e_F01W02_bit2 -F_0x2e_F01W02_bit3 -F_0x2e_F01W02_bit4 -F_0x2e_F01W02_bit5 -F_0x2e_F01W02_bit6 -F_0x2e_F01W02_bit7 -F_0x2e_F01W02_bit8 -F_0x2e_F01W02_bit9 -F_0x2e_F01W02_bit10 -F_0x2e_F01W02_bit11 -F_0x2e_F01W02_bit12 -F_0x2e_F02W02_bit_7 -F_0x2e_F02W02_bit_6 -F_0x2e_F02W02_bit_5 -F_0x2e_F02W02_bit_4 -F_0x2e_F02W02_bit_3 -F_0x2e_F02W02_bit_2 -F_0x2e_F02W02_bit_1 -F_0x2e_F02W02_bit0 -F_0x2e_F02W02_bit1 -F_0x2e_F02W02_bit2 -F_0x2e_F02W02_bit3 -F_0x2e_F02W02_bit4 -F_0x2e_F02W02_bit5 -F_0x2e_F02W02_bit6 -F_0x2e_F02W02_bit7 -F_0x2e_F02W02_bit8 -F_0x2e_F02W02_bit9 -F_0x2e_F02W02_bit10 -F_0x2e_F02W02_bit11 -F_0x2e_F02W02_bit12 -F_0x2e_F02W03_bit_7 -F_0x2e_F02W03_bit_6 -F_0x2e_F02W03_bit_5 -F_0x2e_F02W03_bit_4 -F_0x2e_F02W03_bit_3 -F_0x2e_F02W03_bit_2 -F_0x2e_F02W03_bit_1 -F_0x2e_F02W03_bit0 -F_0x2e_F02W03_bit1 -F_0x2e_F02W03_bit2 -F_0x2e_F02W03_bit3 -F_0x2e_F02W03_bit4 -F_0x2e_F02W03_bit5 -F_0x2e_F02W03_bit6 -F_0x2e_F02W03_bit7 -F_0x2e_F02W03_bit8 -F_0x2e_F02W03_bit9 -F_0x2e_F02W03_bit10 -F_0x2e_F02W03_bit11 -F_0x2e_F02W03_bit12 -F_0x2e_F03W01_bit_7 -F_0x2e_F03W01_bit_6 -F_0x2e_F03W01_bit_5 -F_0x2e_F03W01_bit_4 -F_0x2e_F03W01_bit_3 -F_0x2e_F03W01_bit_2 -F_0x2e_F03W01_bit_1 -F_0x2e_F03W01_bit0 -F_0x2e_F03W01_bit1 -F_0x2e_F03W01_bit2 -F_0x2e_F03W01_bit3 -F_0x2e_F03W01_bit4 -F_0x2e_F03W01_bit5 -F_0x2e_F03W01_bit6 -F_0x2e_F03W01_bit7 -F_0x2e_F03W01_bit8 -F_0x2e_F03W01_bit9 -F_0x2e_F03W01_bit10 -F_0x2e_F03W01_bit11 -F_0x2e_F03W01_bit12 -F_0x2e_F03W03_bit_7 -F_0x2e_F03W03_bit_6 -F_0x2e_F03W03_bit_5 -F_0x2e_F03W03_bit_4 -F_0x2e_F03W03_bit_3 -F_0x2e_F03W03_bit_2 -F_0x2e_F03W03_bit_1 -F_0x2e_F03W03_bit0 -F_0x2e_F03W03_bit1 -F_0x2e_F03W03_bit2 -F_0x2e_F03W03_bit3 -F_0x2e_F03W03_bit4 -F_0x2e_F03W03_bit5 -F_0x2e_F03W03_bit6 -F_0x2e_F03W03_bit7 -F_0x2e_F03W03_bit8 -F_0x2e_F03W03_bit9 -F_0x2e_F03W03_bit10 -F_0x2e_F03W03_bit11 -F_0x2e_F03W03_bit12 -F_0x2e_W01D02_bit_7 -F_0x2e_W01D02_bit_6 -F_0x2e_W01D02_bit_5 -F_0x2e_W01D02_bit_4 -F_0x2e_W01D02_bit_3 -F_0x2e_W01D02_bit_2 -F_0x2e_W01D02_bit_1 -F_0x2e_W01D02_bit0 -F_0x2e_W01D02_bit1 -F_0x2e_W01D02_bit2 -F_0x2e_W01D02_bit3 -F_0x2e_W01D02_bit4 -F_0x2e_W01D02_bit5 -F_0x2e_W01D02_bit6 -F_0x2e_W01D02_bit7 -F_0x2e_W01D02_bit8 -F_0x2e_W01D02_bit9 -F_0x2e_W01D02_bit10 -F_0x2e_W01D02_bit11 -F_0x2e_W01D02_bit12 -F_0x2e_W01D03_bit_7 -F_0x2e_W01D03_bit_6 -F_0x2e_W01D03_bit_5 -F_0x2e_W01D03_bit_4 -F_0x2e_W01D03_bit_3 -F_0x2e_W01D03_bit_2 -F_0x2e_W01D03_bit_1 -F_0x2e_W01D03_bit0 -F_0x2e_W01D03_bit1 -F_0x2e_W01D03_bit2 -F_0x2e_W01D03_bit3 -F_0x2e_W01D03_bit4 -F_0x2e_W01D03_bit5 -F_0x2e_W01D03_bit6 -F_0x2e_W01D03_bit7 -F_0x2e_W01D03_bit8 -F_0x2e_W01D03_bit9 -F_0x2e_W01D03_bit10 -F_0x2e_W01D03_bit11 -F_0x2e_W01D03_bit12 -F_0x2e_W01D04_bit_7 -F_0x2e_W01D04_bit_6 -F_0x2e_W01D04_bit_5 -F_0x2e_W01D04_bit_4 -F_0x2e_W01D04_bit_3 -F_0x2e_W01D04_bit_2 -F_0x2e_W01D04_bit_1 -F_0x2e_W01D04_bit0 -F_0x2e_W01D04_bit1 -F_0x2e_W01D04_bit2 -F_0x2e_W01D04_bit3 -F_0x2e_W01D04_bit4 -F_0x2e_W01D04_bit5 -F_0x2e_W01D04_bit6 -F_0x2e_W01D04_bit7 -F_0x2e_W01D04_bit8 -F_0x2e_W01D04_bit9 -F_0x2e_W01D04_bit10 -F_0x2e_W01D04_bit11 -F_0x2e_W01D04_bit12 -F_0x2e_W02D01_bit_7 -F_0x2e_W02D01_bit_6 -F_0x2e_W02D01_bit_5 -F_0x2e_W02D01_bit_4 -F_0x2e_W02D01_bit_3 -F_0x2e_W02D01_bit_2 -F_0x2e_W02D01_bit_1 -F_0x2e_W02D01_bit0 -F_0x2e_W02D01_bit1 -F_0x2e_W02D01_bit2 -F_0x2e_W02D01_bit3 -F_0x2e_W02D01_bit4 -F_0x2e_W02D01_bit5 -F_0x2e_W02D01_bit6 -F_0x2e_W02D01_bit7 -F_0x2e_W02D01_bit8 -F_0x2e_W02D01_bit9 -F_0x2e_W02D01_bit10 -F_0x2e_W02D01_bit11 -F_0x2e_W02D01_bit12 -F_0x2e_W02D03_bit_7 -F_0x2e_W02D03_bit_6 -F_0x2e_W02D03_bit_5 -F_0x2e_W02D03_bit_4 -F_0x2e_W02D03_bit_3 -F_0x2e_W02D03_bit_2 -F_0x2e_W02D03_bit_1 F_0x2e_W02D03_bit0 F_0x2e_W02D03_bit1 F_0x2e_W02D03_bit2 F_0x2e_W02D03_bit3 -F_0x2e_W02D03_bit4 -F_0x2e_W02D03_bit5 -F_0x2e_W02D03_bit6 -F_0x2e_W02D03_bit7 -F_0x2e_W02D03_bit8 -F_0x2e_W02D03_bit9 -F_0x2e_W02D03_bit10 -F_0x2e_W02D03_bit11 -F_0x2e_W02D03_bit12 -F_0x2e_W02D04_bit_7 -F_0x2e_W02D04_bit_6 -F_0x2e_W02D04_bit_5 -F_0x2e_W02D04_bit_4 -F_0x2e_W02D04_bit_3 -F_0x2e_W02D04_bit_2 -F_0x2e_W02D04_bit_1 F_0x2e_W02D04_bit0 F_0x2e_W02D04_bit1 F_0x2e_W02D04_bit2 F_0x2e_W02D04_bit3 -F_0x2e_W02D04_bit4 -F_0x2e_W02D04_bit5 -F_0x2e_W02D04_bit6 -F_0x2e_W02D04_bit7 -F_0x2e_W02D04_bit8 -F_0x2e_W02D04_bit9 -F_0x2e_W02D04_bit10 -F_0x2e_W02D04_bit11 -F_0x2e_W02D04_bit12 -F_0x2e_W03D01_bit_7 -F_0x2e_W03D01_bit_6 -F_0x2e_W03D01_bit_5 -F_0x2e_W03D01_bit_4 -F_0x2e_W03D01_bit_3 -F_0x2e_W03D01_bit_2 -F_0x2e_W03D01_bit_1 -F_0x2e_W03D01_bit0 -F_0x2e_W03D01_bit1 -F_0x2e_W03D01_bit2 -F_0x2e_W03D01_bit3 -F_0x2e_W03D01_bit4 -F_0x2e_W03D01_bit5 -F_0x2e_W03D01_bit6 -F_0x2e_W03D01_bit7 -F_0x2e_W03D01_bit8 -F_0x2e_W03D01_bit9 -F_0x2e_W03D01_bit10 -F_0x2e_W03D01_bit11 -F_0x2e_W03D01_bit12 -F_0x2e_W03D02_bit_7 -F_0x2e_W03D02_bit_6 -F_0x2e_W03D02_bit_5 -F_0x2e_W03D02_bit_4 -F_0x2e_W03D02_bit_3 -F_0x2e_W03D02_bit_2 -F_0x2e_W03D02_bit_1 -F_0x2e_W03D02_bit0 -F_0x2e_W03D02_bit1 -F_0x2e_W03D02_bit2 -F_0x2e_W03D02_bit3 -F_0x2e_W03D02_bit4 -F_0x2e_W03D02_bit5 -F_0x2e_W03D02_bit6 -F_0x2e_W03D02_bit7 -F_0x2e_W03D02_bit8 -F_0x2e_W03D02_bit9 -F_0x2e_W03D02_bit10 -F_0x2e_W03D02_bit11 -F_0x2e_W03D02_bit12 -F_0x2e_W03D04_bit_7 -F_0x2e_W03D04_bit_6 -F_0x2e_W03D04_bit_5 -F_0x2e_W03D04_bit_4 -F_0x2e_W03D04_bit_3 -F_0x2e_W03D04_bit_2 -F_0x2e_W03D04_bit_1 -F_0x2e_W03D04_bit0 -F_0x2e_W03D04_bit1 -F_0x2e_W03D04_bit2 -F_0x2e_W03D04_bit3 -F_0x2e_W03D04_bit4 -F_0x2e_W03D04_bit5 -F_0x2e_W03D04_bit6 -F_0x2e_W03D04_bit7 -F_0x2e_W03D04_bit8 -F_0x2e_W03D04_bit9 -F_0x2e_W03D04_bit10 -F_0x2e_W03D04_bit11 -F_0x2e_W03D04_bit12 -F_0x2e_D01C01_bit_7 -F_0x2e_D01C01_bit_6 -F_0x2e_D01C01_bit_5 -F_0x2e_D01C01_bit_4 -F_0x2e_D01C01_bit_3 -F_0x2e_D01C01_bit_2 -F_0x2e_D01C01_bit_1 -F_0x2e_D01C01_bit0 -F_0x2e_D01C01_bit1 -F_0x2e_D01C01_bit2 -F_0x2e_D01C01_bit3 -F_0x2e_D01C01_bit4 -F_0x2e_D01C01_bit5 -F_0x2e_D01C01_bit6 -F_0x2e_D01C01_bit7 -F_0x2e_D01C01_bit8 -F_0x2e_D01C01_bit9 -F_0x2e_D01C01_bit10 -F_0x2e_D01C01_bit11 -F_0x2e_D01C01_bit12 -F_0x2e_D01C03_bit_7 -F_0x2e_D01C03_bit_6 -F_0x2e_D01C03_bit_5 -F_0x2e_D01C03_bit_4 -F_0x2e_D01C03_bit_3 -F_0x2e_D01C03_bit_2 -F_0x2e_D01C03_bit_1 -F_0x2e_D01C03_bit0 -F_0x2e_D01C03_bit1 -F_0x2e_D01C03_bit2 -F_0x2e_D01C03_bit3 -F_0x2e_D01C03_bit4 -F_0x2e_D01C03_bit5 -F_0x2e_D01C03_bit6 -F_0x2e_D01C03_bit7 -F_0x2e_D01C03_bit8 -F_0x2e_D01C03_bit9 -F_0x2e_D01C03_bit10 -F_0x2e_D01C03_bit11 -F_0x2e_D01C03_bit12 -F_0x2e_D02C01_bit_7 -F_0x2e_D02C01_bit_6 -F_0x2e_D02C01_bit_5 -F_0x2e_D02C01_bit_4 -F_0x2e_D02C01_bit_3 -F_0x2e_D02C01_bit_2 -F_0x2e_D02C01_bit_1 -F_0x2e_D02C01_bit0 -F_0x2e_D02C01_bit1 -F_0x2e_D02C01_bit2 -F_0x2e_D02C01_bit3 -F_0x2e_D02C01_bit4 -F_0x2e_D02C01_bit5 -F_0x2e_D02C01_bit6 -F_0x2e_D02C01_bit7 -F_0x2e_D02C01_bit8 -F_0x2e_D02C01_bit9 -F_0x2e_D02C01_bit10 -F_0x2e_D02C01_bit11 -F_0x2e_D02C01_bit12 -F_0x2e_D02C02_bit_7 -F_0x2e_D02C02_bit_6 -F_0x2e_D02C02_bit_5 -F_0x2e_D02C02_bit_4 -F_0x2e_D02C02_bit_3 -F_0x2e_D02C02_bit_2 -F_0x2e_D02C02_bit_1 -F_0x2e_D02C02_bit0 -F_0x2e_D02C02_bit1 -F_0x2e_D02C02_bit2 -F_0x2e_D02C02_bit3 -F_0x2e_D02C02_bit4 -F_0x2e_D02C02_bit5 -F_0x2e_D02C02_bit6 -F_0x2e_D02C02_bit7 -F_0x2e_D02C02_bit8 -F_0x2e_D02C02_bit9 -F_0x2e_D02C02_bit10 -F_0x2e_D02C02_bit11 -F_0x2e_D02C02_bit12 -F_0x2e_D03C01_bit_7 -F_0x2e_D03C01_bit_6 -F_0x2e_D03C01_bit_5 -F_0x2e_D03C01_bit_4 -F_0x2e_D03C01_bit_3 -F_0x2e_D03C01_bit_2 -F_0x2e_D03C01_bit_1 -F_0x2e_D03C01_bit0 -F_0x2e_D03C01_bit1 -F_0x2e_D03C01_bit2 -F_0x2e_D03C01_bit3 -F_0x2e_D03C01_bit4 -F_0x2e_D03C01_bit5 -F_0x2e_D03C01_bit6 -F_0x2e_D03C01_bit7 -F_0x2e_D03C01_bit8 -F_0x2e_D03C01_bit9 -F_0x2e_D03C01_bit10 -F_0x2e_D03C01_bit11 -F_0x2e_D03C01_bit12 -F_0x2e_D03C03_bit_7 -F_0x2e_D03C03_bit_6 -F_0x2e_D03C03_bit_5 -F_0x2e_D03C03_bit_4 -F_0x2e_D03C03_bit_3 -F_0x2e_D03C03_bit_2 -F_0x2e_D03C03_bit_1 -F_0x2e_D03C03_bit0 -F_0x2e_D03C03_bit1 -F_0x2e_D03C03_bit2 -F_0x2e_D03C03_bit3 -F_0x2e_D03C03_bit4 -F_0x2e_D03C03_bit5 -F_0x2e_D03C03_bit6 -F_0x2e_D03C03_bit7 -F_0x2e_D03C03_bit8 -F_0x2e_D03C03_bit9 -F_0x2e_D03C03_bit10 -F_0x2e_D03C03_bit11 -F_0x2e_D03C03_bit12 -F_0x2e_D04C01_bit_7 -F_0x2e_D04C01_bit_6 -F_0x2e_D04C01_bit_5 -F_0x2e_D04C01_bit_4 -F_0x2e_D04C01_bit_3 -F_0x2e_D04C01_bit_2 -F_0x2e_D04C01_bit_1 F_0x2e_D04C01_bit0 F_0x2e_D04C01_bit1 F_0x2e_D04C01_bit2 F_0x2e_D04C01_bit3 -F_0x2e_D04C01_bit4 -F_0x2e_D04C01_bit5 -F_0x2e_D04C01_bit6 -F_0x2e_D04C01_bit7 -F_0x2e_D04C01_bit8 -F_0x2e_D04C01_bit9 -F_0x2e_D04C01_bit10 -F_0x2e_D04C01_bit11 -F_0x2e_D04C01_bit12 -F_0x2e_D04C02_bit_7 -F_0x2e_D04C02_bit_6 -F_0x2e_D04C02_bit_5 -F_0x2e_D04C02_bit_4 -F_0x2e_D04C02_bit_3 -F_0x2e_D04C02_bit_2 -F_0x2e_D04C02_bit_1 -F_0x2e_D04C02_bit0 -F_0x2e_D04C02_bit1 -F_0x2e_D04C02_bit2 -F_0x2e_D04C02_bit3 -F_0x2e_D04C02_bit4 -F_0x2e_D04C02_bit5 -F_0x2e_D04C02_bit6 -F_0x2e_D04C02_bit7 -F_0x2e_D04C02_bit8 -F_0x2e_D04C02_bit9 -F_0x2e_D04C02_bit10 -F_0x2e_D04C02_bit11 -F_0x2e_D04C02_bit12 -F_0x2e_D04C03_bit_7 -F_0x2e_D04C03_bit_6 -F_0x2e_D04C03_bit_5 -F_0x2e_D04C03_bit_4 -F_0x2e_D04C03_bit_3 -F_0x2e_D04C03_bit_2 -F_0x2e_D04C03_bit_1 -F_0x2e_D04C03_bit0 -F_0x2e_D04C03_bit1 -F_0x2e_D04C03_bit2 -F_0x2e_D04C03_bit3 -F_0x2e_D04C03_bit4 -F_0x2e_D04C03_bit5 -F_0x2e_D04C03_bit6 -F_0x2e_D04C03_bit7 -F_0x2e_D04C03_bit8 -F_0x2e_D04C03_bit9 -F_0x2e_D04C03_bit10 -F_0x2e_D04C03_bit11 -F_0x2e_D04C03_bit12 -I_0x2e_D01C01_bit0 -I_0x2e_D01C02_bit0 -I_0x2e_D01C03_bit0 -I_0x2e_D02C01_bit0 -I_0x2e_D02C02_bit0 I_0x2e_D02C03_bit0 -I_0x2e_D03C01_bit0 I_0x2e_D03C02_bit0 -I_0x2e_D03C03_bit0 I_0x2e_D04C01_bit0 -I_0x2e_D04C02_bit0 -I_0x2e_D04C03_bit0 -F_0x2e_D04D04_bit_7 -F_0x2e_D04D04_bit_6 -F_0x2e_D04D04_bit_5 -F_0x2e_D04D04_bit_4 -F_0x2e_D04D04_bit_3 -F_0x2e_D04D04_bit_2 -F_0x2e_D04D04_bit_1 F_0x2e_D04D04_bit0 F_0x2e_D04D04_bit1 F_0x2e_D04D04_bit2 F_0x2e_D04D04_bit3 -F_0x2e_D04D04_bit4 -F_0x2e__0x2e__0x2e__0x2e_F01_bit_7 -F_0x2e__0x2e__0x2e__0x2e_F01_bit_6 -F_0x2e__0x2e__0x2e__0x2e_F01_bit_5 -F_0x2e__0x2e__0x2e__0x2e_F01_bit_4 -F_0x2e__0x2e__0x2e__0x2e_F01_bit_3 -F_0x2e__0x2e__0x2e__0x2e_F01_bit_2 -F_0x2e__0x2e__0x2e__0x2e_F01_bit_1 -F_0x2e__0x2e__0x2e__0x2e_F01_bit0 -F_0x2e__0x2e__0x2e__0x2e_F01_bit1 -F_0x2e__0x2e__0x2e__0x2e_F01_bit2 -F_0x2e__0x2e__0x2e__0x2e_F01_bit3 -F_0x2e__0x2e__0x2e__0x2e_F01_bit4 -F_0x2e__0x2e__0x2e__0x2e_F01_bit5 -F_0x2e__0x2e__0x2e__0x2e_F01_bit6 -F_0x2e__0x2e__0x2e__0x2e_F01_bit7 -F_0x2e__0x2e__0x2e__0x2e_F01_bit8 -F_0x2e__0x2e__0x2e__0x2e_F01_bit9 -F_0x2e__0x2e__0x2e__0x2e_F01_bit10 -F_0x2e__0x2e__0x2e__0x2e_F01_bit11 -F_0x2e__0x2e__0x2e__0x2e_F01_bit12 -F_0x2e__0x2e__0x2e__0x2e_F02_bit_7 -F_0x2e__0x2e__0x2e__0x2e_F02_bit_6 -F_0x2e__0x2e__0x2e__0x2e_F02_bit_5 -F_0x2e__0x2e__0x2e__0x2e_F02_bit_4 -F_0x2e__0x2e__0x2e__0x2e_F02_bit_3 -F_0x2e__0x2e__0x2e__0x2e_F02_bit_2 -F_0x2e__0x2e__0x2e__0x2e_F02_bit_1 -F_0x2e__0x2e__0x2e__0x2e_F02_bit0 -F_0x2e__0x2e__0x2e__0x2e_F02_bit1 -F_0x2e__0x2e__0x2e__0x2e_F02_bit2 -F_0x2e__0x2e__0x2e__0x2e_F02_bit3 -F_0x2e__0x2e__0x2e__0x2e_F02_bit4 -F_0x2e__0x2e__0x2e__0x2e_F02_bit5 -F_0x2e__0x2e__0x2e__0x2e_F02_bit6 -F_0x2e__0x2e__0x2e__0x2e_F02_bit7 -F_0x2e__0x2e__0x2e__0x2e_F02_bit8 -F_0x2e__0x2e__0x2e__0x2e_F02_bit9 -F_0x2e__0x2e__0x2e__0x2e_F02_bit10 -F_0x2e__0x2e__0x2e__0x2e_F02_bit11 -F_0x2e__0x2e__0x2e__0x2e_F02_bit12 -F_0x2e__0x2e__0x2e__0x2e_F03_bit_7 -F_0x2e__0x2e__0x2e__0x2e_F03_bit_6 -F_0x2e__0x2e__0x2e__0x2e_F03_bit_5 -F_0x2e__0x2e__0x2e__0x2e_F03_bit_4 -F_0x2e__0x2e__0x2e__0x2e_F03_bit_3 -F_0x2e__0x2e__0x2e__0x2e_F03_bit_2 -F_0x2e__0x2e__0x2e__0x2e_F03_bit_1 F_0x2e__0x2e__0x2e__0x2e_F03_bit0 -F_0x2e__0x2e__0x2e__0x2e_F03_bit1 F_0x2e__0x2e__0x2e__0x2e_F03_bit2 F_0x2e__0x2e__0x2e__0x2e_F03_bit3 -F_0x2e__0x2e__0x2e__0x2e_F03_bit4 F_0x2e__0x2e__0x2e__0x2e_F03_bit5 -F_0x2e__0x2e__0x2e__0x2e_F03_bit6 -F_0x2e__0x2e__0x2e__0x2e_F03_bit7 -F_0x2e__0x2e__0x2e__0x2e_F03_bit8 -F_0x2e__0x2e__0x2e__0x2e_F03_bit9 -F_0x2e__0x2e__0x2e__0x2e_F03_bit10 -F_0x2e__0x2e__0x2e__0x2e_F03_bit11 -F_0x2e__0x2e__0x2e__0x2e_F03_bit12 -F_0x2e_D01C02_bit_7 -F_0x2e_D01C02_bit_6 -F_0x2e_D01C02_bit_5 -F_0x2e_D01C02_bit_4 -F_0x2e_D01C02_bit_3 -F_0x2e_D01C02_bit_2 -F_0x2e_D01C02_bit_1 -F_0x2e_D01C02_bit0 -F_0x2e_D01C02_bit1 -F_0x2e_D01C02_bit2 -F_0x2e_D01C02_bit3 -F_0x2e_D01C02_bit4 -F_0x2e_D01C02_bit5 -F_0x2e_D01C02_bit6 -F_0x2e_D01C02_bit7 -F_0x2e_D01C02_bit8 -F_0x2e_D01C02_bit9 -F_0x2e_D01C02_bit10 -F_0x2e_D01C02_bit11 -F_0x2e_D01C02_bit12 -F_0x2e_D03C02_bit_7 -F_0x2e_D03C02_bit_6 -F_0x2e_D03C02_bit_5 -F_0x2e_D03C02_bit_4 -F_0x2e_D03C02_bit_3 -F_0x2e_D03C02_bit_2 -F_0x2e_D03C02_bit_1 F_0x2e_D03C02_bit0 F_0x2e_D03C02_bit1 F_0x2e_D03C02_bit2 F_0x2e_D03C02_bit3 -F_0x2e_D03C02_bit4 -F_0x2e_D03C02_bit5 -F_0x2e_D03C02_bit6 -F_0x2e_D03C02_bit7 -F_0x2e_D03C02_bit8 -F_0x2e_D03C02_bit9 -F_0x2e_D03C02_bit10 -F_0x2e_D03C02_bit11 -F_0x2e_D03C02_bit12 -F_0x2e_D02C03_bit_7 -F_0x2e_D02C03_bit_6 -F_0x2e_D02C03_bit_5 -F_0x2e_D02C03_bit_4 -F_0x2e_D02C03_bit_3 -F_0x2e_D02C03_bit_2 -F_0x2e_D02C03_bit_1 F_0x2e_D02C03_bit0 F_0x2e_D02C03_bit1 F_0x2e_D02C03_bit2 F_0x2e_D02C03_bit3 -F_0x2e_D02C03_bit4 -F_0x2e_D02C03_bit5 -F_0x2e_D02C03_bit6 -F_0x2e_D02C03_bit7 -F_0x2e_D02C03_bit8 -F_0x2e_D02C03_bit9 -F_0x2e_D02C03_bit10 -F_0x2e_D02C03_bit11 -F_0x2e_D02C03_bit12 -F_0x2e_W01D01_bit_7 -F_0x2e_W01D01_bit_6 -F_0x2e_W01D01_bit_5 -F_0x2e_W01D01_bit_4 -F_0x2e_W01D01_bit_3 -F_0x2e_W01D01_bit_2 -F_0x2e_W01D01_bit_1 -F_0x2e_W01D01_bit0 -F_0x2e_W01D01_bit1 -F_0x2e_W01D01_bit2 -F_0x2e_W01D01_bit3 -F_0x2e_W01D01_bit4 -F_0x2e_W01D01_bit5 -F_0x2e_W01D01_bit6 -F_0x2e_W01D01_bit7 -F_0x2e_W01D01_bit8 -F_0x2e_W01D01_bit9 -F_0x2e_W01D01_bit10 -F_0x2e_W01D01_bit11 -F_0x2e_W01D01_bit12 -F_0x2e_D01D01_bit_7 -F_0x2e_D01D01_bit_6 -F_0x2e_D01D01_bit_5 -F_0x2e_D01D01_bit_4 -F_0x2e_D01D01_bit_3 -F_0x2e_D01D01_bit_2 -F_0x2e_D01D01_bit_1 -F_0x2e_D01D01_bit0 -F_0x2e_D01D01_bit1 -F_0x2e_D01D01_bit2 -F_0x2e_D01D01_bit3 -F_0x2e_D01D01_bit4 -F_0x2e_D01D01_bit5 -F_0x2e_D01D01_bit6 -F_0x2e_D01D01_bit7 -F_0x2e_D01D01_bit8 -F_0x2e_D01D01_bit9 -F_0x2e_D01D01_bit10 -F_0x2e_D01D01_bit11 -F_0x2e_D01D01_bit12 -F_0x2e_W02D02_bit_7 -F_0x2e_W02D02_bit_6 -F_0x2e_W02D02_bit_5 -F_0x2e_W02D02_bit_4 -F_0x2e_W02D02_bit_3 -F_0x2e_W02D02_bit_2 -F_0x2e_W02D02_bit_1 F_0x2e_W02D02_bit0 F_0x2e_W02D02_bit1 F_0x2e_W02D02_bit2 F_0x2e_W02D02_bit3 -F_0x2e_W02D02_bit4 -F_0x2e_W02D02_bit5 -F_0x2e_W02D02_bit6 -F_0x2e_W02D02_bit7 -F_0x2e_W02D02_bit8 -F_0x2e_W02D02_bit9 -F_0x2e_W02D02_bit10 -F_0x2e_W02D02_bit11 -F_0x2e_W02D02_bit12 -F_0x2e_D02D02_bit_7 -F_0x2e_D02D02_bit_6 -F_0x2e_D02D02_bit_5 -F_0x2e_D02D02_bit_4 -F_0x2e_D02D02_bit_3 -F_0x2e_D02D02_bit_2 -F_0x2e_D02D02_bit_1 F_0x2e_D02D02_bit0 F_0x2e_D02D02_bit1 F_0x2e_D02D02_bit2 F_0x2e_D02D02_bit3 -F_0x2e_D02D02_bit4 -F_0x2e_D02D02_bit5 -F_0x2e_D02D02_bit6 -F_0x2e_D02D02_bit7 -F_0x2e_D02D02_bit8 -F_0x2e_D02D02_bit9 -F_0x2e_D02D02_bit10 -F_0x2e_D02D02_bit11 -F_0x2e_D02D02_bit12 -F_0x2e_W03D03_bit_7 -F_0x2e_W03D03_bit_6 -F_0x2e_W03D03_bit_5 -F_0x2e_W03D03_bit_4 -F_0x2e_W03D03_bit_3 -F_0x2e_W03D03_bit_2 -F_0x2e_W03D03_bit_1 -F_0x2e_W03D03_bit0 -F_0x2e_W03D03_bit1 -F_0x2e_W03D03_bit2 -F_0x2e_W03D03_bit3 -F_0x2e_W03D03_bit4 -F_0x2e_W03D03_bit5 -F_0x2e_W03D03_bit6 -F_0x2e_W03D03_bit7 -F_0x2e_W03D03_bit8 -F_0x2e_W03D03_bit9 -F_0x2e_W03D03_bit10 -F_0x2e_W03D03_bit11 -F_0x2e_W03D03_bit12 -F_0x2e_D03D03_bit_7 -F_0x2e_D03D03_bit_6 -F_0x2e_D03D03_bit_5 -F_0x2e_D03D03_bit_4 -F_0x2e_D03D03_bit_3 -F_0x2e_D03D03_bit_2 -F_0x2e_D03D03_bit_1 F_0x2e_D03D03_bit0 F_0x2e_D03D03_bit1 F_0x2e_D03D03_bit2 F_0x2e_D03D03_bit3 -F_0x2e_D03D03_bit4 -F_0x2e_D03D03_bit5 -F_0x2e_D03D03_bit6 -F_0x2e_D03D03_bit7 -F_0x2e_D03D03_bit8 -F_0x2e_D03D03_bit9 -F_0x2e_D03D03_bit10 -F_0x2e_D03D03_bit11 -F_0x2e_D03D03_bit12 -F_0x2e_F01W03_bit_7 -F_0x2e_F01W03_bit_6 -F_0x2e_F01W03_bit_5 -F_0x2e_F01W03_bit_4 -F_0x2e_F01W03_bit_3 -F_0x2e_F01W03_bit_2 -F_0x2e_F01W03_bit_1 -F_0x2e_F01W03_bit0 -F_0x2e_F01W03_bit1 -F_0x2e_F01W03_bit2 -F_0x2e_F01W03_bit3 -F_0x2e_F01W03_bit4 -F_0x2e_F01W03_bit5 -F_0x2e_F01W03_bit6 -F_0x2e_F01W03_bit7 -F_0x2e_F01W03_bit8 -F_0x2e_F01W03_bit9 -F_0x2e_F01W03_bit10 -F_0x2e_F01W03_bit11 -F_0x2e_F01W03_bit12 -F_0x2e_F02W01_bit_7 -F_0x2e_F02W01_bit_6 -F_0x2e_F02W01_bit_5 -F_0x2e_F02W01_bit_4 -F_0x2e_F02W01_bit_3 -F_0x2e_F02W01_bit_2 -F_0x2e_F02W01_bit_1 -F_0x2e_F02W01_bit0 -F_0x2e_F02W01_bit1 -F_0x2e_F02W01_bit2 -F_0x2e_F02W01_bit3 -F_0x2e_F02W01_bit4 -F_0x2e_F02W01_bit5 -F_0x2e_F02W01_bit6 -F_0x2e_F02W01_bit7 -F_0x2e_F02W01_bit8 -F_0x2e_F02W01_bit9 -F_0x2e_F02W01_bit10 -F_0x2e_F02W01_bit11 -F_0x2e_F02W01_bit12 -F_0x2e_F03W02_bit_7 -F_0x2e_F03W02_bit_6 -F_0x2e_F03W02_bit_5 -F_0x2e_F03W02_bit_4 -F_0x2e_F03W02_bit_3 -F_0x2e_F03W02_bit_2 -F_0x2e_F03W02_bit_1 F_0x2e_F03W02_bit0 -F_0x2e_F03W02_bit1 F_0x2e_F03W02_bit2 F_0x2e_F03W02_bit3 -F_0x2e_F03W02_bit4 F_0x2e_F03W02_bit5 -F_0x2e_F03W02_bit6 -F_0x2e_F03W02_bit7 -F_0x2e_F03W02_bit8 -F_0x2e_F03W02_bit9 -F_0x2e_F03W02_bit10 -F_0x2e_F03W02_bit11 -F_0x2e_F03W02_bit12 -F_0x2e_W01W01_bit_7 -F_0x2e_W01W01_bit_6 -F_0x2e_W01W01_bit_5 -F_0x2e_W01W01_bit_4 -F_0x2e_W01W01_bit_3 -F_0x2e_W01W01_bit_2 -F_0x2e_W01W01_bit_1 -F_0x2e_W01W01_bit0 -F_0x2e_W01W01_bit1 -F_0x2e_W01W01_bit2 -F_0x2e_W01W01_bit3 -F_0x2e_W01W01_bit4 -F_0x2e_W01W01_bit5 -F_0x2e_W01W01_bit6 -F_0x2e_W01W01_bit7 -F_0x2e_W01W01_bit8 -F_0x2e_W01W01_bit9 -F_0x2e_W01W01_bit10 -F_0x2e_W01W01_bit11 -F_0x2e_W01W01_bit12 -F_0x2e_W02W02_bit_7 -F_0x2e_W02W02_bit_6 -F_0x2e_W02W02_bit_5 -F_0x2e_W02W02_bit_4 -F_0x2e_W02W02_bit_3 -F_0x2e_W02W02_bit_2 -F_0x2e_W02W02_bit_1 F_0x2e_W02W02_bit0 -F_0x2e_W02W02_bit1 F_0x2e_W02W02_bit2 F_0x2e_W02W02_bit3 -F_0x2e_W02W02_bit4 F_0x2e_W02W02_bit5 -F_0x2e_W02W02_bit6 -F_0x2e_W02W02_bit7 -F_0x2e_W02W02_bit8 -F_0x2e_W02W02_bit9 -F_0x2e_W02W02_bit10 -F_0x2e_W02W02_bit11 -F_0x2e_W02W02_bit12 -F_0x2e_W03W03_bit_7 -F_0x2e_W03W03_bit_6 -F_0x2e_W03W03_bit_5 -F_0x2e_W03W03_bit_4 -F_0x2e_W03W03_bit_3 -F_0x2e_W03W03_bit_2 -F_0x2e_W03W03_bit_1 -F_0x2e_W03W03_bit0 -F_0x2e_W03W03_bit1 -F_0x2e_W03W03_bit2 -F_0x2e_W03W03_bit3 -F_0x2e_W03W03_bit4 -F_0x2e_W03W03_bit5 -F_0x2e_W03W03_bit6 -F_0x2e_W03W03_bit7 -F_0x2e_W03W03_bit8 -F_0x2e_W03W03_bit9 -F_0x2e_W03W03_bit10 -F_0x2e_W03W03_bit11 -F_0x2e_W03W03_bit12
c _______________________________________________________________________________
c 
c restarts              : 37
c conflicts             : 6501           (121 /sec)
c decisions             : 26128          (486 /sec)
c propagations          : 9384885        (174740 /sec)
c inspects              : 33836822       (630016 /sec)
c CPU time              : 53.7078 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 11897
Raw data (stat): 11897 (runsolver) R 11896 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488599075 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 11897
Raw data (stat): 11897 (minisat+) R 11896 22932 22931 0 -1 0 7849 0 0 0 970 28 0 0 25 0 1 0 488599075 27213824 5625 4294967295 134512640 134672761 3221224544 3221222656 134603406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6644 5625 603 41 0 6603 0
vsize: 26576
[startup+20.0008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 11897
Raw data (stat): 11897 (minisat+) R 11896 22932 22931 0 -1 0 13972 0 0 0 1947 51 0 0 25 0 1 0 488599075 31731712 7195 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7747 7195 603 41 0 7706 0
vsize: 30988
[startup+30.001 s]
Raw data (loadavg): 1.05 0.98 0.92 2/54 11897
Raw data (stat): 11897 (minisat+) R 11896 22932 22931 0 -1 0 19801 0 0 0 2925 73 0 0 25 0 1 0 488599075 58101760 10257 4294967295 134512640 134672761 3221224544 3221222808 1075730078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14185 10257 603 41 0 14144 0
vsize: 56740
[startup+40.0011 s]
Raw data (loadavg): 1.04 0.98 0.92 2/54 11897
Raw data (stat): 11897 (minisat+) R 11896 22932 22931 0 -1 0 24988 0 0 0 3907 90 0 0 25 0 1 0 488599075 45465600 8900 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11100 8900 603 41 0 11059 0
vsize: 44400
[startup+50.0017 s]
Raw data (loadavg): 1.03 0.98 0.92 2/54 11897
Raw data (stat): 11897 (minisat+) R 11896 22932 22931 0 -1 0 29614 0 0 0 4889 108 0 0 25 0 1 0 488599075 48259072 9791 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 9791 603 41 0 11741 0
vsize: 47128
[startup+54.8858 s]
Raw data (loadavg): 1.03 0.98 0.92 1/53 11897
Raw data (stat): 11897 (minisat+) R 11896 22932 22931 0 -1 0 29614 0 0 0 4889 108 0 0 25 0 1 0 488599075 48259072 9791 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 9791 603 41 0 11741 0
vsize: 0

Child status: 30
Real time (s): 54.8855
CPU time (s): 54.8577
CPU user time (s): 53.7458
CPU system time (s): 1.11183
CPU usage (%): 99.9493
Max. virtual memory (Kb): 56740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	48000
#### END VERIFIER DATA ####