Name | normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-sc50b.opb |
MD5SUM | f10dfcccbc5d23245c6e708690ee08ea |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -70000 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 30 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 1073741823 |
Number of bits of the sum of numbers in the objective function | 30 |
Biggest number in a constraint | 5905580032 |
Number of bits of the biggest number in a constraint | 33 |
Biggest sum of numbers in a constraint | 22548578283 |
Number of bits of the biggest sum of numbers | 35 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 336.565 |
Number of variables | 1440 |
Total number of constraints | 48 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 48 |
Minimum length of a constraint | 60 |
Maximum length of a constraint | 120 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc28 THE 2005-05-27 06:28:24 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23216 boxname=wulflinc28 idbench=860 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f10dfcccbc5d23245c6e708690ee08ea /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-sc50b.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-sc50b.opb IDLAUNCH: 23216 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 914776 kB Buffers: 176 kB Cached: 98792 kB SwapCached: 788 kB Active: 15208 kB Inactive: 86064 kB HighTotal: 131008 kB HighFree: 28756 kB LowTotal: 903652 kB LowFree: 886020 kB SwapTotal: 2097640 kB SwapFree: 2096156 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5412 kB Slab: 12872 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 06:34:01 (client local time) WITH STATUS 30 IN 336.565 SECONDS stats: 23216 0 336.565 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 68 PB-constraints to clauses... c -- Unit propagations: ppppppp c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): (none) c ---[ 67]---> BDD-cost: 185 c ---[ 65]---> BDD-cost: 52 c ---[ 63]---> BDD-cost: 49 c ---[ 61]---> BDD-cost: 49 c ---[ 59]---> BDD-cost: 49 c ---[ 58]---> BDD-cost: 49 c ---[ 57]---> BDD-cost: 49 c ---[ 56]---> BDD-cost: 49 c ---[ 55]---> BDD-cost: 786 c ---[ 54]---> BDD-cost: 290 c ---[ 53]---> BDD-cost: 252 c ---[ 51]---> BDD-cost: 628 c ---[ 49]---> BDD-cost: 164 c ---[ 47]---> BDD-cost: 155 c ---[ 45]---> BDD-cost: 155 c ---[ 43]---> BDD-cost: 155 c ---[ 42]---> BDD-cost: 55 c ---[ 41]---> BDD-cost: 55 c ---[ 40]---> BDD-cost: 55 c ---[ 39]---> BDD-cost: 882 c ---[ 38]---> BDD-cost: 330 c ---[ 37]---> BDD-cost: 286 c ---[ 35]---> BDD-cost: 678 c ---[ 33]---> BDD-cost: 177 c ---[ 31]---> BDD-cost: 168 c ---[ 29]---> BDD-cost: 168 c ---[ 27]---> BDD-cost: 168 c ---[ 26]---> BDD-cost: 58 c ---[ 25]---> BDD-cost: 58 c ---[ 24]---> BDD-cost: 58 c ---[ 23]---> BDD-cost: 924 c ---[ 22]---> BDD-cost: 350 c ---[ 21]---> BDD-cost: 303 c ---[ 19]---> BDD-cost: 728 c ---[ 17]---> BDD-cost: 186 c ---[ 15]---> BDD-cost: 173 c ---[ 13]---> BDD-cost: 173 c ---[ 11]---> BDD-cost: 173 c ---[ 10]---> BDD-cost: 61 c ---[ 9]---> BDD-cost: 61 c ---[ 8]---> BDD-cost: 61 c ---[ 7]---> BDD-cost: 977 c ---[ 6]---> BDD-cost: 370 c ---[ 5]---> BDD-cost: 320 c ---[ 3]---> BDD-cost: 768 c ---[ 2]---> BDD-cost: 1208 c ---[ 1]---> BDD-cost: 350 c ---[ 0]---> BDD-cost: 303 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 30741 83826 | 10247 0 0 nan | 0.000 % | c | 101 | 30642 83568 | 11271 99 3813 38.5 | 4.355 % | c | 252 | 30621 83514 | 12398 247 6487 26.3 | 4.420 % | c ============================================================================== c [1mFound solution: 0[0m c ---[ 0]---> Sorter-cost: 126 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 292 | 30622 83531 | 10207 287 6747 23.5 | 4.420 % | c | 392 | 30592 83471 | 11227 372 7780 20.9 | 4.537 % | c | 542 | 30592 83471 | 12350 522 9688 18.6 | 4.537 % | c | 767 | 30592 83471 | 13585 747 12162 16.3 | 4.537 % | c | 1105 | 30592 83471 | 14944 1085 15668 14.4 | 4.537 % | c | 1613 | 30588 83463 | 16438 1591 28753 18.1 | 4.551 % | c | 2372 | 30588 83463 | 18082 2350 39222 16.7 | 4.551 % | c ============================================================================== c [1mFound solution: -60000[0m c ---[ 0]---> Sorter-cost: 91 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2571 | 30735 83807 | 10245 2544 41427 16.3 | 4.551 % | c | 2671 | 30413 82968 | 11269 2635 42549 16.1 | 5.544 % | c | 2822 | 30190 82411 | 12396 2753 43677 15.9 | 6.238 % | c | 3048 | 30190 82411 | 13636 2979 46355 15.6 | 6.238 % | c | 3386 | 30190 82411 | 14999 3317 49219 14.8 | 6.238 % | c | 3892 | 30190 82411 | 16499 3823 53085 13.9 | 6.238 % | c | 4651 | 30190 82411 | 18149 4582 79007 17.2 | 6.238 % | c | 5791 | 30131 82265 | 19964 5610 98101 17.5 | 6.369 % | c | 7499 | 29887 81688 | 21961 5319 107054 20.1 | 6.853 % | c | 10061 | 29833 81554 | 24157 7791 198267 25.4 | 6.969 % | c | 13907 | 29769 81391 | 26572 11624 312113 26.9 | 7.121 % | c | 19673 | 29765 81383 | 29230 17388 479955 27.6 | 7.136 % | c | 28322 | 29693 81196 | 32153 25990 787383 30.3 | 7.266 % | c | 41297 | 29689 81188 | 35368 19784 645991 32.7 | 7.280 % | c | 60761 | 29689 81188 | 38905 14717 534242 36.3 | 7.280 % | c | 89954 | 29675 81160 | 42795 18065 554093 30.7 | 7.331 % | c | 133744 | 29665 81140 | 47075 31216 1313035 42.1 | 7.367 % | c | 199428 | 29525 80831 | 51783 24717 1076003 43.5 | 7.678 % | c ============================================================================== c [1mFound solution: -70000[0m c ---[ 0]---> Sorter-cost: 199 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 291443 | 29940 81811 | 9980 34014 2553866 75.1 | 7.678 % | c | 291545 | 29940 81811 | 10978 8007 464291 58.0 | 7.644 % | c | 291695 | 29938 81807 | 12075 8156 465319 57.1 | 7.652 % | c | 291921 | 29681 81216 | 13283 8123 464989 57.2 | 8.202 % | c | 292258 | 29681 81216 | 14611 8460 473222 55.9 | 8.202 % | c | 292764 | 29334 80362 | 16072 8948 483368 54.0 | 8.846 % | c | 293524 | 29334 80362 | 17680 9708 504150 51.9 | 8.846 % | c | 294663 | 29334 80362 | 19448 10847 531681 49.0 | 8.846 % | c | 296372 | 29329 80350 | 21393 12555 581089 46.3 | 8.860 % | c | 298935 | 29191 80003 | 23532 15114 632429 41.8 | 9.189 % | c | 302780 | 28767 78925 | 25885 15198 348705 22.9 | 10.205 % | c | 308546 | 28765 78921 | 28474 20957 446804 21.3 | 10.212 % | c ============================================================================== c [1mOptimal solution: -70000[0m s OPTIMUM FOUND v -COL00004_bit_10 -COL00004_bit_9 -COL00004_bit_8 -COL00004_bit_7 COL00004_bit_6 COL00004_bit_5 COL00004_bit_4 -COL00004_bit_3 COL00004_bit_2 -COL00004_bit_1 -COL00004_bit0 -COL00004_bit1 COL00004_bit2 -COL00004_bit3 -COL00004_bit4 -COL00004_bit5 COL00004_bit6 -COL00004_bit7 -COL00004_bit8 -COL00004_bit9 -COL00004_bit10 -COL00004_bit11 -COL00004_bit12 -COL00004_bit13 -COL00004_bit14 -COL00004_bit15 -COL00004_bit16 -COL00004_bit17 -COL00004_bit18 -COL00004_bit19 -COL00001_bit_10 -COL00001_bit_9 -COL00001_bit_8 -COL00001_bit_7 -COL00001_bit_6 -COL00001_bit_5 COL00001_bit_4 COL00001_bit_3 COL00001_bit_2 -COL00001_bit_1 -COL00001_bit0 -COL00001_bit1 COL00001_bit2 -COL00001_bit3 -COL00001_bit4 -COL00001_bit5 -COL00001_bit6 -COL00001_bit7 -COL00001_bit8 -COL00001_bit9 -COL00001_bit10 -COL00001_bit11 -COL00001_bit12 -COL00001_bit13 -COL00001_bit14 -COL00001_bit15 -COL00001_bit16 -COL00001_bit17 -COL00001_bit18 -COL00001_bit19 -COL00002_bit_10 -COL00002_bit_9 -COL00002_bit_8 -COL00002_bit_7 -COL00002_bit_6 -COL00002_bit_5 COL00002_bit_4 COL00002_bit_3 COL00002_bit_2 -COL00002_bit_1 -COL00002_bit0 COL00002_bit1 COL00002_bit2 -COL00002_bit3 COL00002_bit4 COL00002_bit5 -COL00002_bit6 -COL00002_bit7 -COL00002_bit8 -COL00002_bit9 -COL00002_bit10 -COL00002_bit11 -COL00002_bit12 -COL00002_bit13 -COL00002_bit14 -COL00002_bit15 -COL00002_bit16 -COL00002_bit17 -COL00002_bit18 -COL00002_bit19 -COL00003_bit_10 -COL00003_bit_9 -COL00003_bit_8 -COL00003_bit_7 -COL00003_bit_6 -COL00003_bit_5 -COL00003_bit_4 COL00003_bit_3 -COL00003_bit_2 -COL00003_bit_1 COL00003_bit0 -COL00003_bit1 -COL00003_bit2 COL00003_bit3 -COL00003_bit4 COL00003_bit5 -COL00003_bit6 -COL00003_bit7 -COL00003_bit8 -COL00003_bit9 -COL00003_bit10 -COL00003_bit11 -COL00003_bit12 -COL00003_bit13 -COL00003_bit14 -COL00003_bit15 -COL00003_bit16 -COL00003_bit17 -COL00003_bit18 -COL00003_bit19 -COL00005_bit_10 -COL00005_bit_9 -COL00005_bit_8 -COL00005_bit_7 COL00005_bit_6 COL00005_bit_5 COL00005_bit_4 -COL00005_bit_3 COL00005_bit_2 -COL00005_bit_1 -COL00005_bit0 -COL00005_bit1 COL00005_bit2 -COL00005_bit3 -COL00005_bit4 -COL00005_bit5 COL00005_bit6 -COL00005_bit7 -COL00005_bit8 -COL00005_bit9 -COL00005_bit10 -COL00005_bit11 -COL00005_bit12 -COL00005_bit13 -COL00005_bit14 -COL00005_bit15 -COL00005_bit16 -COL00005_bit17 -COL00005_bit18 -COL00005_bit19 -COL00006_bit_10 -COL00006_bit_9 -COL00006_bit_8 -COL00006_bit_7 -COL00006_bit_6 -COL00006_bit_5 COL00006_bit_4 COL00006_bit_3 COL00006_bit_2 -COL00006_bit_1 -COL00006_bit0 -COL00006_bit1 COL00006_bit2 -COL00006_bit3 -COL00006_bit4 -COL00006_bit5 -COL00006_bit6 -COL00006_bit7 -COL00006_bit8 -COL00006_bit9 -COL00006_bit10 -COL00006_bit11 -COL00006_bit12 -COL00006_bit13 -COL00006_bit14 -COL00006_bit15 -COL00006_bit16 -COL00006_bit17 -COL00006_bit18 -COL00006_bit19 -COL00007_bit_10 -COL00007_bit_9 -COL00007_bit_8 -COL00007_bit_7 -COL00007_bit_6 -COL00007_bit_5 COL00007_bit_4 COL00007_bit_3 COL00007_bit_2 -COL00007_bit_1 -COL00007_bit0 COL00007_bit1 COL00007_bit2 -COL00007_bit3 COL00007_bit4 COL00007_bit5 -COL00007_bit6 -COL00007_bit7 -COL00007_bit8 -COL00007_bit9 -COL00007_bit10 -COL00007_bit11 -COL00007_bit12 -COL00007_bit13 -COL00007_bit14 -COL00007_bit15 -COL00007_bit16 -COL00007_bit17 -COL00007_bit18 -COL00007_bit19 -COL00008_bit_10 -COL00008_bit_9 -COL00008_bit_8 -COL00008_bit_7 -COL00008_bit_6 -COL00008_bit_5 -COL00008_bit_4 COL00008_bit_3 -COL00008_bit_2 -COL00008_bit_1 COL00008_bit0 -COL00008_bit1 -COL00008_bit2 COL00008_bit3 -COL00008_bit4 COL00008_bit5 -COL00008_bit6 -COL00008_bit7 -COL00008_bit8 -COL00008_bit9 -COL00008_bit10 -COL00008_bit11 -COL00008_bit12 -COL00008_bit13 -COL00008_bit14 -COL00008_bit15 -COL00008_bit16 -COL00008_bit17 -COL00008_bit18 -COL00008_bit19 -COL00009_bit_10 -COL00009_bit_9 -COL00009_bit_8 -COL00009_bit_7 -COL00009_bit_6 -COL00009_bit_5 -COL00009_bit_4 COL00009_bit_3 COL00009_bit_2 -COL00009_bit_1 -COL00009_bit0 -COL00009_bit1 COL00009_bit2 -COL00009_bit3 -COL00009_bit4 -COL00009_bit5 -COL00009_bit6 -COL00009_bit7 -COL00009_bit8 -COL00009_bit9 -COL00009_bit10 -COL00009_bit11 -COL00009_bit12 -COL00009_bit13 -COL00009_bit14 -COL00009_bit15 -COL00009_bit16 -COL00009_bit17 -COL00009_bit18 -COL00009_bit19 -COL00010_bit_10 COL00010_bit_9 -COL00010_bit_8 -COL00010_bit_7 COL00010_bit_6 COL00010_bit_5 COL00010_bit_4 COL00010_bit_3 -COL00010_bit_2 -COL00010_bit_1 COL00010_bit0 COL00010_bit1 COL00010_bit2 COL00010_bit3 COL00010_bit4 -COL00010_bit5 -COL00010_bit6 -COL00010_bit7 -COL00010_bit8 -COL00010_bit9 -COL00010_bit10 -COL00010_bit11 -COL00010_bit12 -COL00010_bit13 -COL00010_bit14 -COL00010_bit15 -COL00010_bit16 -COL00010_bit17 -COL00010_bit18 -COL00010_bit19 -COL00011_bit_10 COL00011_bit_9 -COL00011_bit_8 -COL00011_bit_7 COL00011_bit_6 -COL00011_bit_5 -COL00011_bit_4 -COL00011_bit_3 -COL00011_bit_2 -COL00011_bit_1 COL00011_bit0 -COL00011_bit1 -COL00011_bit2 COL00011_bit3 -COL00011_bit4 COL00011_bit5 -COL00011_bit6 -COL00011_bit7 -COL00011_bit8 -COL00011_bit9 -COL00011_bit10 -COL00011_bit11 -COL00011_bit12 -COL00011_bit13 -COL00011_bit14 -COL00011_bit15 -COL00011_bit16 -COL00011_bit17 -COL00011_bit18 -COL00011_bit19 -COL00012_bit_10 -COL00012_bit_9 -COL00012_bit_8 -COL00012_bit_7 COL00012_bit_6 -COL00012_bit_5 COL00012_bit_4 -COL00012_bit_3 -COL00012_bit_2 COL00012_bit_1 COL00012_bit0 COL00012_bit1 -COL00012_bit2 COL00012_bit3 -COL00012_bit4 COL00012_bit5 -COL00012_bit6 -COL00012_bit7 -COL00012_bit8 -COL00012_bit9 -COL00012_bit10 -COL00012_bit11 -COL00012_bit12 -COL00012_bit13 -COL00012_bit14 -COL00012_bit15 -COL00012_bit16 -COL00012_bit17 -COL00012_bit18 -COL00012_bit19 -COL00013_bit_10 -COL00013_bit_9 -COL00013_bit_8 -COL00013_bit_7 -COL00013_bit_6 -COL00013_bit_5 -COL00013_bit_4 -COL00013_bit_3 -COL00013_bit_2 -COL00013_bit_1 COL00013_bit0 COL00013_bit1 -COL00013_bit2 -COL00013_bit3 -COL00013_bit4 -COL00013_bit5 -COL00013_bit6 -COL00013_bit7 -COL00013_bit8 -COL00013_bit9 -COL00013_bit10 -COL00013_bit11 -COL00013_bit12 -COL00013_bit13 -COL00013_bit14 -COL00013_bit15 -COL00013_bit16 -COL00013_bit17 -COL00013_bit18 -COL00013_bit19 -COL00014_bit_10 -COL00014_bit_9 -COL00014_bit_8 -COL00014_bit_7 -COL00014_bit_6 -COL00014_bit_5 -COL00014_bit_4 COL00014_bit_3 COL00014_bit_2 COL00014_bit_1 -COL00014_bit0 COL00014_bit1 COL00014_bit2 -COL00014_bit3 COL00014_bit4 COL00014_bit5 -COL00014_bit6 -COL00014_bit7 -COL00014_bit8 -COL00014_bit9 -COL00014_bit10 -COL00014_bit11 -COL00014_bit12 -COL00014_bit13 -COL00014_bit14 -COL00014_bit15 -COL00014_bit16 -COL00014_bit17 -COL00014_bit18 -COL00014_bit19 -COL00015_bit_10 -COL00015_bit_9 -COL00015_bit_8 COL00015_bit_7 -COL00015_bit_6 -COL00015_bit_5 COL00015_bit_4 COL00015_bit_3 -COL00015_bit_2 -COL00015_bit_1 COL00015_bit0 COL00015_bit1 -COL00015_bit2 COL00015_bit3 -COL00015_bit4 -COL00015_bit5 COL00015_bit6 -COL00015_bit7 -COL00015_bit8 -COL00015_bit9 -COL00015_bit10 -COL00015_bit11 -COL00015_bit12 -COL00015_bit13 -COL00015_bit14 -COL00015_bit15 -COL00015_bit16 -COL00015_bit17 -COL00015_bit18 -COL00015_bit19 -COL00016_bit_10 -COL00016_bit_9 -COL00016_bit_8 COL00016_bit_7 COL00016_bit_6 COL00016_bit_5 -COL00016_bit_4 -COL00016_bit_3 -COL00016_bit_2 COL00016_bit_1 COL00016_bit0 COL00016_bit1 COL00016_bit2 COL00016_bit3 -COL00016_bit4 -COL00016_bit5 -COL00016_bit6 COL00016_bit7 -COL00016_bit8 -COL00016_bit9 -COL00016_bit10 -COL00016_bit11 -COL00016_bit12 -COL00016_bit13 -COL00016_bit14 -COL00016_bit15 -COL00016_bit16 -COL00016_bit17 -COL00016_bit18 -COL00016_bit19 -COL00017_bit_10 -COL00017_bit_9 -COL00017_bit_8 -COL00017_bit_7 COL00017_bit_6 -COL00017_bit_5 -COL00017_bit_4 -COL00017_bit_3 -COL00017_bit_2 -COL00017_bit_1 -COL00017_bit0 -COL00017_bit1 -COL00017_bit2 -COL00017_bit3 COL00017_bit4 COL00017_bit5 -COL00017_bit6 -COL00017_bit7 -COL00017_bit8 -COL00017_bit9 -COL00017_bit10 -COL00017_bit11 -COL00017_bit12 -COL00017_bit13 -COL00017_bit14 -COL00017_bit15 -COL00017_bit16 -COL00017_bit17 -COL00017_bit18 -COL00017_bit19 -COL00018_bit_10 -COL00018_bit_9 -COL00018_bit_8 -COL00018_bit_7 -COL00018_bit_6 -COL00018_bit_5 COL00018_bit_4 COL00018_bit_3 COL00018_bit_2 -COL00018_bit_1 COL00018_bit0 -COL00018_bit1 -COL00018_bit2 COL00018_bit3 COL00018_bit4 COL00018_bit5 -COL00018_bit6 -COL00018_bit7 -COL00018_bit8 -COL00018_bit9 -COL00018_bit10 -COL00018_bit11 -COL00018_bit12 -COL00018_bit13 -COL00018_bit14 -COL00018_bit15 -COL00018_bit16 -COL00018_bit17 -COL00018_bit18 -COL00018_bit19 -COL00019_bit_10 -COL00019_bit_9 -COL00019_bit_8 -COL00019_bit_7 -COL00019_bit_6 -COL00019_bit_5 -COL00019_bit_4 -COL00019_bit_3 -COL00019_bit_2 -COL00019_bit_1 -COL00019_bit0 -COL00019_bit1 -COL00019_bit2 -COL00019_bit3 -COL00019_bit4 COL00019_bit5 COL00019_bit6 -COL00019_bit7 -COL00019_bit8 -COL00019_bit9 -COL00019_bit10 -COL00019_bit11 -COL00019_bit12 -COL00019_bit13 -COL00019_bit14 -COL00019_bit15 -COL00019_bit16 -COL00019_bit17 -COL00019_bit18 -COL00019_bit19 -COL00020_bit_10 -COL00020_bit_9 -COL00020_bit_8 -COL00020_bit_7 -COL00020_bit_6 -COL00020_bit_5 -COL00020_bit_4 -COL00020_bit_3 -COL00020_bit_2 COL00020_bit_1 -COL00020_bit0 COL00020_bit1 COL00020_bit2 COL00020_bit3 -COL00020_bit4 COL00020_bit5 -COL00020_bit6 -COL00020_bit7 -COL00020_bit8 -COL00020_bit9 -COL00020_bit10 -COL00020_bit11 -COL00020_bit12 -COL00020_bit13 -COL00020_bit14 -COL00020_bit15 -COL00020_bit16 -COL00020_bit17 -COL00020_bit18 -COL00020_bit19 -COL00021_bit_10 COL00021_bit_9 -COL00021_bit_8 COL00021_bit_7 COL00021_bit_6 COL00021_bit_5 -COL00021_bit_4 COL00021_bit_3 COL00021_bit_2 -COL00021_bit_1 COL00021_bit0 -COL00021_bit1 -COL00021_bit2 COL00021_bit3 COL00021_bit4 COL00021_bit5 -COL00021_bit6 -COL00021_bit7 -COL00021_bit8 -COL00021_bit9 -COL00021_bit10 -COL00021_bit11 -COL00021_bit12 -COL00021_bit13 -COL00021_bit14 -COL00021_bit15 -COL00021_bit16 -COL00021_bit17 -COL00021_bit18 -COL00021_bit19 -COL00022_bit_10 COL00022_bit_9 -COL00022_bit_8 -COL00022_bit_7 COL00022_bit_6 -COL00022_bit_5 COL00022_bit_4 -COL00022_bit_3 COL00022_bit_2 COL00022_bit_1 COL00022_bit0 COL00022_bit1 COL00022_bit2 COL00022_bit3 COL00022_bit4 -COL00022_bit5 COL00022_bit6 -COL00022_bit7 -COL00022_bit8 -COL00022_bit9 -COL00022_bit10 -COL00022_bit11 -COL00022_bit12 -COL00022_bit13 -COL00022_bit14 -COL00022_bit15 -COL00022_bit16 -COL00022_bit17 -COL00022_bit18 -COL00022_bit19 -COL00023_bit_10 COL00023_bit_9 COL00023_bit_8 COL00023_bit_7 -COL00023_bit_6 COL00023_bit_5 COL00023_bit_4 COL00023_bit_3 COL00023_bit_2 COL00023_bit_1 COL00023_bit0 COL00023_bit1 COL00023_bit2 -COL00023_bit3 -COL00023_bit4 COL00023_bit5 -COL00023_bit6 -COL00023_bit7 -COL00023_bit8 -COL00023_bit9 -COL00023_bit10 -COL00023_bit11 -COL00023_bit12 -COL00023_bit13 -COL00023_bit14 -COL00023_bit15 -COL00023_bit16 -COL00023_bit17 -COL00023_bit18 -COL00023_bit19 -COL00024_bit_10 -COL00024_bit_9 -COL00024_bit_8 -COL00024_bit_7 -COL00024_bit_6 -COL00024_bit_5 -COL00024_bit_4 -COL00024_bit_3 -COL00024_bit_2 COL00024_bit_1 COL00024_bit0 COL00024_bit1 -COL00024_bit2 -COL00024_bit3 -COL00024_bit4 COL00024_bit5 -COL00024_bit6 -COL00024_bit7 -COL00024_bit8 -COL00024_bit9 -COL00024_bit10 -COL00024_bit11 -COL00024_bit12 -COL00024_bit13 -COL00024_bit14 -COL00024_bit15 -COL00024_bit16 -COL00024_bit17 -COL00024_bit18 -COL00024_bit19 -COL00025_bit_10 -COL00025_bit_9 -COL00025_bit_8 COL00025_bit_7 COL00025_bit_6 COL00025_bit_5 COL00025_bit_4 COL00025_bit_3 COL00025_bit_2 COL00025_bit_1 COL00025_bit0 COL00025_bit1 COL00025_bit2 -COL00025_bit3 -COL00025_bit4 COL00025_bit5 -COL00025_bit6 -COL00025_bit7 -COL00025_bit8 -COL00025_bit9 -COL00025_bit10 -COL00025_bit11 -COL00025_bit12 -COL00025_bit13 -COL00025_bit14 -COL00025_bit15 -COL00025_bit16 -COL00025_bit17 -COL00025_bit18 -COL00025_bit19 -COL00026_bit_10 -COL00026_bit_9 COL00026_bit_8 COL00026_bit_7 COL00026_bit_6 -COL00026_bit_5 COL00026_bit_4 COL00026_bit_3 -COL00026_bit_2 COL00026_bit_1 -COL00026_bit0 COL00026_bit1 -COL00026_bit2 -COL00026_bit3 COL00026_bit4 -COL00026_bit5 COL00026_bit6 -COL00026_bit7 -COL00026_bit8 -COL00026_bit9 -COL00026_bit10 -COL00026_bit11 -COL00026_bit12 -COL00026_bit13 -COL00026_bit14 -COL00026_bit15 -COL00026_bit16 -COL00026_bit17 -COL00026_bit18 -COL00026_bit19 -COL00027_bit_10 -COL00027_bit_9 COL00027_bit_8 -COL00027_bit_7 COL00027_bit_6 -COL00027_bit_5 -COL00027_bit_4 -COL00027_bit_3 COL00027_bit_2 -COL00027_bit_1 -COL00027_bit0 COL00027_bit1 -COL00027_bit2 -COL00027_bit3 -COL00027_bit4 COL00027_bit5 COL00027_bit6 COL00027_bit7 -COL00027_bit8 -COL00027_bit9 -COL00027_bit10 -COL00027_bit11 -COL00027_bit12 -COL00027_bit13 -COL00027_bit14 -COL00027_bit15 -COL00027_bit16 -COL00027_bit17 -COL00027_bit18 -COL00027_bit19 -COL00028_bit_10 COL00028_bit_9 COL00028_bit_8 COL00028_bit_7 COL00028_bit_6 COL00028_bit_5 COL00028_bit_4 COL00028_bit_3 COL00028_bit_2 COL00028_bit_1 COL00028_bit0 COL00028_bit1 COL00028_bit2 -COL00028_bit3 COL00028_bit4 -COL00028_bit5 COL00028_bit6 -COL00028_bit7 -COL00028_bit8 -COL00028_bit9 -COL00028_bit10 -COL00028_bit11 -COL00028_bit12 -COL00028_bit13 -COL00028_bit14 -COL00028_bit15 -COL00028_bit16 -COL00028_bit17 -COL00028_bit18 -COL00028_bit19 -COL00029_bit_10 -COL00029_bit_9 -COL00029_bit_8 -COL00029_bit_7 -COL00029_bit_6 -COL00029_bit_5 COL00029_bit_4 COL00029_bit_3 COL00029_bit_2 COL00029_bit_1 -COL00029_bit0 -COL00029_bit1 COL00029_bit2 COL00029_bit3 COL00029_bit4 -COL00029_bit5 COL00029_bit6 -COL00029_bit7 -COL00029_bit8 -COL00029_bit9 -COL00029_bit10 -COL00029_bit11 -COL00029_bit12 -COL00029_bit13 -COL00029_bit14 -COL00029_bit15 -COL00029_bit16 -COL00029_bit17 -COL00029_bit18 -COL00029_bit19 -COL00030_bit_10 -COL00030_bit_9 -COL00030_bit_8 COL00030_bit_7 COL00030_bit_6 COL00030_bit_5 COL00030_bit_4 COL00030_bit_3 COL00030_bit_2 COL00030_bit_1 COL00030_bit0 COL00030_bit1 COL00030_bit2 -COL00030_bit3 -COL00030_bit4 -COL00030_bit5 -COL00030_bit6 COL00030_bit7 -COL00030_bit8 -COL00030_bit9 -COL00030_bit10 -COL00030_bit11 -COL00030_bit12 -COL00030_bit13 -COL00030_bit14 -COL00030_bit15 -COL00030_bit16 -COL00030_bit17 -COL00030_bit18 -COL00030_bit19 -COL00031_bit_10 COL00031_bit_9 COL00031_bit_8 COL00031_bit_7 COL00031_bit_6 -COL00031_bit_5 COL00031_bit_4 COL00031_bit_3 COL00031_bit_2 COL00031_bit_1 COL00031_bit0 COL00031_bit1 COL00031_bit2 -COL00031_bit3 COL00031_bit4 -COL00031_bit5 COL00031_bit6 -COL00031_bit7 -COL00031_bit8 -COL00031_bit9 -COL00031_bit10 -COL00031_bit11 -COL00031_bit12 -COL00031_bit13 -COL00031_bit14 -COL00031_bit15 -COL00031_bit16 -COL00031_bit17 -COL00031_bit18 -COL00031_bit19 -COL00032_bit_10 -COL00032_bit_9 -COL00032_bit_8 -COL00032_bit_7 -COL00032_bit_6 COL00032_bit_5 -COL00032_bit_4 -COL00032_bit_3 -COL00032_bit_2 COL00032_bit_1 COL00032_bit0 COL00032_bit1 -COL00032_bit2 COL00032_bit3 COL00032_bit4 -COL00032_bit5 COL00032_bit6 -COL00032_bit7 -COL00032_bit8 -COL00032_bit9 -COL00032_bit10 -COL00032_bit11 -COL00032_bit12 -COL00032_bit13 -COL00032_bit14 -COL00032_bit15 -COL00032_bit16 -COL00032_bit17 -COL00032_bit18 -COL00032_bit19 -COL00033_bit_10 -COL00033_bit_9 COL00033_bit_8 COL00033_bit_7 -COL00033_bit_6 -COL00033_bit_5 -COL00033_bit_4 COL00033_bit_3 COL00033_bit_2 COL00033_bit_1 COL00033_bit0 COL00033_bit1 COL00033_bit2 -COL00033_bit3 -COL00033_bit4 -COL00033_bit5 -COL00033_bit6 COL00033_bit7 -COL00033_bit8 -COL00033_bit9 -COL00033_bit10 -COL00033_bit11 -COL00033_bit12 -COL00033_bit13 -COL00033_bit14 -COL00033_bit15 -COL00033_bit16 -COL00033_bit17 -COL00033_bit18 -COL00033_bit19 -COL00034_bit_10 COL00034_bit_9 -COL00034_bit_8 -COL00034_bit_7 COL00034_bit_6 -COL00034_bit_5 COL00034_bit_4 COL00034_bit_3 COL00034_bit_2 COL00034_bit_1 -COL00034_bit0 -COL00034_bit1 -COL00034_bit2 COL00034_bit3 -COL00034_bit4 COL00034_bit5 -COL00034_bit6 -COL00034_bit7 -COL00034_bit8 -COL00034_bit9 -COL00034_bit10 -COL00034_bit11 -COL00034_bit12 -COL00034_bit13 -COL00034_bit14 -COL00034_bit15 -COL00034_bit16 -COL00034_bit17 -COL00034_bit18 -COL00034_bit19 -COL00035_bit_10 -COL00035_bit_9 -COL00035_bit_8 -COL00035_bit_7 -COL00035_bit_6 -COL00035_bit_5 -COL00035_bit_4 -COL00035_bit_3 -COL00035_bit_2 -COL00035_bit_1 -COL00035_bit0 COL00035_bit1 -COL00035_bit2 -COL00035_bit3 -COL00035_bit4 COL00035_bit5 -COL00035_bit6 -COL00035_bit7 -COL00035_bit8 -COL00035_bit9 -COL00035_bit10 -COL00035_bit11 -COL00035_bit12 -COL00035_bit13 -COL00035_bit14 -COL00035_bit15 -COL00035_bit16 -COL00035_bit17 -COL00035_bit18 -COL00035_bit19 -COL00036_bit_10 -COL00036_bit_9 -COL00036_bit_8 COL00036_bit_7 COL00036_bit_6 COL00036_bit_5 COL00036_bit_4 -COL00036_bit_3 COL00036_bit_2 -COL00036_bit_1 -COL00036_bit0 COL00036_bit1 COL00036_bit2 -COL00036_bit3 COL00036_bit4 COL00036_bit5 -COL00036_bit6 -COL00036_bit7 -COL00036_bit8 -COL00036_bit9 -COL00036_bit10 -COL00036_bit11 -COL00036_bit12 -COL00036_bit13 -COL00036_bit14 -COL00036_bit15 -COL00036_bit16 -COL00036_bit17 -COL00036_bit18 -COL00036_bit19 -COL00037_bit_10 COL00037_bit_9 -COL00037_bit_8 -COL00037_bit_7 COL00037_bit_6 COL00037_bit_5 COL00037_bit_4 COL00037_bit_3 COL00037_bit_2 COL00037_bit_1 -COL00037_bit0 COL00037_bit1 -COL00037_bit2 COL00037_bit3 COL00037_bit4 -COL00037_bit5 COL00037_bit6 -COL00037_bit7 -COL00037_bit8 -COL00037_bit9 -COL00037_bit10 -COL00037_bit11 -COL00037_bit12 -COL00037_bit13 -COL00037_bit14 -COL00037_bit15 -COL00037_bit16 -COL00037_bit17 -COL00037_bit18 -COL00037_bit19 -COL00038_bit_10 COL00038_bit_9 COL00038_bit_8 -COL00038_bit_7 -COL00038_bit_6 -COL00038_bit_5 -COL00038_bit_4 -COL00038_bit_3 COL00038_bit_2 -COL00038_bit_1 COL00038_bit0 -COL00038_bit1 COL00038_bit2 COL00038_bit3 COL00038_bit4 COL00038_bit5 -COL00038_bit6 -COL00038_bit7 COL00038_bit8 -COL00038_bit9 -COL00038_bit10 -COL00038_bit11 -COL00038_bit12 -COL00038_bit13 -COL00038_bit14 -COL00038_bit15 -COL00038_bit16 -COL00038_bit17 -COL00038_bit18 -COL00038_bit19 -COL00039_bit_10 -COL00039_bit_9 -COL00039_bit_8 -COL00039_bit_7 COL00039_bit_6 -COL00039_bit_5 COL00039_bit_4 COL00039_bit_3 COL00039_bit_2 COL00039_bit_1 -COL00039_bit0 -COL00039_bit1 -COL00039_bit2 -COL00039_bit3 -COL00039_bit4 -COL00039_bit5 -COL00039_bit6 COL00039_bit7 -COL00039_bit8 -COL00039_bit9 -COL00039_bit10 -COL00039_bit11 -COL00039_bit12 -COL00039_bit13 -COL00039_bit14 -COL00039_bit15 -COL00039_bit16 -COL00039_bit17 -COL00039_bit18 -COL00039_bit19 -COL00040_bit_10 -COL00040_bit_9 -COL00040_bit_8 -COL00040_bit_7 -COL00040_bit_6 -COL00040_bit_5 COL00040_bit_4 COL00040_bit_3 COL00040_bit_2 COL00040_bit_1 -COL00040_bit0 COL00040_bit1 COL00040_bit2 COL00040_bit3 COL00040_bit4 COL00040_bit5 COL00040_bit6 -COL00040_bit7 -COL00040_bit8 -COL00040_bit9 -COL00040_bit10 -COL00040_bit11 -COL00040_bit12 -COL00040_bit13 -COL00040_bit14 -COL00040_bit15 -COL00040_bit16 -COL00040_bit17 -COL00040_bit18 -COL00040_bit19 -COL00041_bit_10 -COL00041_bit_9 -COL00041_bit_8 -COL00041_bit_7 COL00041_bit_6 COL00041_bit_5 COL00041_bit_4 -COL00041_bit_3 COL00041_bit_2 -COL00041_bit_1 -COL00041_bit0 COL00041_bit1 COL00041_bit2 COL00041_bit3 COL00041_bit4 COL00041_bit5 -COL00041_bit6 COL00041_bit7 -COL00041_bit8 -COL00041_bit9 -COL00041_bit10 -COL00041_bit11 -COL00041_bit12 -COL00041_bit13 -COL00041_bit14 -COL00041_bit15 -COL00041_bit16 -COL00041_bit17 -COL00041_bit18 -COL00041_bit19 -COL00042_bit_10 -COL00042_bit_9 -COL00042_bit_8 -COL00042_bit_7 COL00042_bit_6 -COL00042_bit_5 COL00042_bit_4 COL00042_bit_3 COL00042_bit_2 COL00042_bit_1 -COL00042_bit0 -COL00042_bit1 -COL00042_bit2 -COL00042_bit3 -COL00042_bit4 -COL00042_bit5 -COL00042_bit6 COL00042_bit7 -COL00042_bit8 -COL00042_bit9 -COL00042_bit10 -COL00042_bit11 -COL00042_bit12 -COL00042_bit13 -COL00042_bit14 -COL00042_bit15 -COL00042_bit16 -COL00042_bit17 -COL00042_bit18 -COL00042_bit19 -COL00043_bit_10 -COL00043_bit_9 -COL00043_bit_8 -COL00043_bit_7 -COL00043_bit_6 -COL00043_bit_5 COL00043_bit_4 COL00043_bit_3 COL00043_bit_2 COL00043_bit_1 -COL00043_bit0 COL00043_bit1 COL00043_bit2 COL00043_bit3 COL00043_bit4 COL00043_bit5 COL00043_bit6 -COL00043_bit7 -COL00043_bit8 -COL00043_bit9 -COL00043_bit10 -COL00043_bit11 -COL00043_bit12 -COL00043_bit13 -COL00043_bit14 -COL00043_bit15 -COL00043_bit16 -COL00043_bit17 -COL00043_bit18 -COL00043_bit19 COL00044_bit_10 COL00044_bit_9 -COL00044_bit_8 COL00044_bit_7 -COL00044_bit_6 COL00044_bit_5 COL00044_bit_4 -COL00044_bit_3 COL00044_bit_2 -COL00044_bit_1 -COL00044_bit0 COL00044_bit1 COL00044_bit2 COL00044_bit3 COL00044_bit4 COL00044_bit5 -COL00044_bit6 COL00044_bit7 -COL00044_bit8 -COL00044_bit9 -COL00044_bit10 -COL00044_bit11 -COL00044_bit12 -COL00044_bit13 -COL00044_bit14 -COL00044_bit15 -COL00044_bit16 -COL00044_bit17 -COL00044_bit18 -COL00044_bit19 -COL00045_bit_10 -COL00045_bit_9 -COL00045_bit_8 COL00045_bit_7 COL00045_bit_6 -COL00045_bit_5 -COL00045_bit_4 COL00045_bit_3 COL00045_bit_2 COL00045_bit_1 -COL00045_bit0 COL00045_bit1 -COL00045_bit2 COL00045_bit3 -COL00045_bit4 COL00045_bit5 -COL00045_bit6 -COL00045_bit7 -COL00045_bit8 -COL00045_bit9 -COL00045_bit10 -COL00045_bit11 -COL00045_bit12 -COL00045_bit13 -COL00045_bit14 -COL00045_bit15 -COL00045_bit16 -COL00045_bit17 -COL00045_bit18 -COL00045_bit19 COL00046_bit_10 COL00046_bit_9 -COL00046_bit_8 -COL00046_bit_7 -COL00046_bit_6 COL00046_bit_5 -COL00046_bit_4 -COL00046_bit_3 -COL00046_bit_2 -COL00046_bit_1 -COL00046_bit0 -COL00046_bit1 -COL00046_bit2 COL00046_bit3 -COL00046_bit4 COL00046_bit5 -COL00046_bit6 -COL00046_bit7 -COL00046_bit8 -COL00046_bit9 -COL00046_bit10 -COL00046_bit11 -COL00046_bit12 -COL00046_bit13 -COL00046_bit14 -COL00046_bit15 -COL00046_bit16 -COL00046_bit17 -COL00046_bit18 -COL00046_bit19 COL00047_bit_10 -COL00047_bit_9 COL00047_bit_8 -COL00047_bit_7 COL00047_bit_6 COL00047_bit_5 -COL00047_bit_4 -COL00047_bit_3 -COL00047_bit_2 -COL00047_bit_1 -COL00047_bit0 -COL00047_bit1 COL00047_bit2 COL00047_bit3 COL00047_bit4 COL00047_bit5 -COL00047_bit6 -COL00047_bit7 -COL00047_bit8 -COL00047_bit9 -COL00047_bit10 -COL00047_bit11 -COL00047_bit12 -COL00047_bit13 -COL00047_bit14 -COL00047_bit15 -COL00047_bit16 -COL00047_bit17 -COL00047_bit18 -COL00047_bit19 COL00048_bit_10 COL00048_bit_9 COL00048_bit_8 -COL00048_bit_7 COL00048_bit_6 -COL00048_bit_5 COL00048_bit_4 -COL00048_bit_3 -COL00048_bit_2 -COL00048_bit_1 -COL00048_bit0 -COL00048_bit1 COL00048_bit2 -COL00048_bit3 -COL00048_bit4 COL00048_bit5 COL00048_bit6 -COL00048_bit7 -COL00048_bit8 -COL00048_bit9 -COL00048_bit10 -COL00048_bit11 -COL00048_bit12 -COL00048_bit13 -COL00048_bit14 -COL00048_bit15 -COL00048_bit16 -COL00048_bit17 -COL00048_bit18 -COL00048_bit19 c _______________________________________________________________________________ c c restarts : 40 c conflicts : 309779 (921 /sec) c decisions : 478057 (1422 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 336.272 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.83 0.96 0.91 2/54 17866 Raw data (stat): 17866 (runsolver) R 17865 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854008759 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 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.0004 s] Raw data (loadavg): 0.85 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0006 s] Raw data (loadavg): 0.88 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0018 s] Raw data (loadavg): 0.89 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0024 s] Raw data (loadavg): 0.91 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0026 s] Raw data (loadavg): 0.92 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0027 s] Raw data (loadavg): 0.93 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0034 s] Raw data (loadavg): 0.94 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0037 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0048 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.005 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.006 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.007 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+336.552 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 17870 Raw data (stat): 17866 (minisat+_script) S 17865 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854008759 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 30 Real time (s): 336.551 CPU time (s): 336.565 CPU user time (s): 336.286 CPU system time (s): 0.278957 CPU usage (%): 100.004 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK -70000 #### END VERIFIER DATA ####