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 |
#### 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 ####