Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-gt2.opb |
MD5SUM | f1382105ee9fb79777762a53cf6a73c1 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 21166 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 304 |
Biggest coefficient in the objective function | 62376 |
Number of bits for the biggest coefficient in the objective function | 16 |
Sum of the numbers in the objective function | 3092598 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 62376 |
Number of bits of the biggest number in a constraint | 16 |
Biggest sum of numbers in a constraint | 3092598 |
Number of bits of the biggest sum of numbers | 22 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1177.34 |
Number of variables | 556 |
Total number of constraints | 217 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 26 |
Number of constraints which are nor clauses,nor cardinality constraints | 191 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 48 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc10 THE 2005-04-21 23:29:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13447 boxname=wulflinc10 idbench=1035 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: f1382105ee9fb79777762a53cf6a73c1 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-gt2.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-gt2.opb IDLAUNCH: 13447 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 731308 kB Buffers: 22720 kB Cached: 259208 kB SwapCached: 0 kB Active: 43528 kB Inactive: 240948 kB HighTotal: 131008 kB HighFree: 728 kB LowTotal: 903652 kB LowFree: 730580 kB SwapTotal: 2097136 kB SwapFree: 2096784 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6412 kB Slab: 13168 kB Committed_AS: 63520 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 23:49:14 (client local time) WITH STATUS 10 IN 1200.25 SECONDS stats: 13447 7 1200.25 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 180 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................ssssssssss c ---[ 189]---> BDD-cost: 2 c ---[ 188]---> BDD-cost: 2 c ---[ 187]---> BDD-cost: 2 c ---[ 186]---> BDD-cost: 2 c ---[ 185]---> BDD-cost: 2 c ---[ 184]---> BDD-cost: 2 c ---[ 183]---> BDD-cost: 2 c ---[ 182]---> BDD-cost: 2 c ---[ 157]---> BDD-cost: 3 c ---[ 156]---> BDD-cost: 3 c ---[ 155]---> BDD-cost: 3 c ---[ 154]---> BDD-cost: 3 c ---[ 153]---> BDD-cost: 3 c ---[ 152]---> BDD-cost: 3 c ---[ 151]---> BDD-cost: 3 c ---[ 150]---> BDD-cost: 3 c ---[ 149]---> BDD-cost: 3 c ---[ 148]---> BDD-cost: 3 c ---[ 147]---> BDD-cost: 3 c ---[ 146]---> BDD-cost: 3 c ---[ 141]---> BDD-cost: 3 c ---[ 140]---> BDD-cost: 3 c ---[ 139]---> BDD-cost: 3 c ---[ 138]---> BDD-cost: 3 c ---[ 137]---> BDD-cost: 3 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 134]---> BDD-cost: 3 c ---[ 120]---> BDD-cost: 2 c ---[ 119]---> BDD-cost: 2 c ---[ 117]---> BDD-cost: 2 c ---[ 113]---> BDD-cost: 2 c ---[ 112]---> BDD-cost: 2 c ---[ 110]---> BDD-cost: 2 c ---[ 106]---> BDD-cost: 2 c ---[ 105]---> BDD-cost: 2 c ---[ 103]---> BDD-cost: 2 c ---[ 99]---> BDD-cost: 2 c ---[ 98]---> BDD-cost: 2 c ---[ 96]---> BDD-cost: 2 c ---[ 92]---> BDD-cost: 2 c ---[ 91]---> BDD-cost: 2 c ---[ 89]---> BDD-cost: 2 c ---[ 85]---> BDD-cost: 2 c ---[ 84]---> BDD-cost: 2 c ---[ 82]---> BDD-cost: 2 c ---[ 78]---> BDD-cost: 2 c ---[ 77]---> BDD-cost: 2 c ---[ 75]---> BDD-cost: 2 c ---[ 71]---> BDD-cost: 2 c ---[ 70]---> BDD-cost: 2 c ---[ 68]---> BDD-cost: 2 c ---[ 64]---> BDD-cost: 2 c ---[ 63]---> BDD-cost: 2 c ---[ 61]---> BDD-cost: 2 c ---[ 57]---> BDD-cost: 2 c ---[ 56]---> BDD-cost: 2 c ---[ 54]---> BDD-cost: 2 c ---[ 50]---> BDD-cost: 2 c ---[ 49]---> BDD-cost: 2 c ---[ 47]---> BDD-cost: 2 c ---[ 43]---> BDD-cost: 2 c ---[ 42]---> BDD-cost: 2 c ---[ 40]---> BDD-cost: 2 c ---[ 37]---> BDD-cost: 107 c ---[ 36]---> Sorter-cost: 778 Base: 2 2 2 c ---[ 35]---> Sorter-cost: 777 Base: 2 2 2 c ---[ 34]---> BDD-cost: 21 c ---[ 33]---> BDD-cost: 128 c ---[ 32]---> BDD-cost: 183 c ---[ 31]---> BDD-cost: 25 c ---[ 30]---> Sorter-cost: 379 Base: 2 2 2 c ---[ 29]---> BDD-cost: 111 c ---[ 28]---> BDD-cost: 128 c ---[ 27]---> BDD-cost: 105 c ---[ 26]---> Sorter-cost: 778 Base: 2 2 2 c ---[ 25]---> BDD-cost: 111 c ---[ 24]---> BDD-cost: 105 c ---[ 23]---> BDD-cost: 54 c ---[ 22]---> BDD-cost: 54 c ---[ 21]---> BDD-cost: 21 c ---[ 15]---> Adder-cost: 273 maxlim: 12127 bits: 15/14 c ---[ 9]---> Sorter-cost: 2085 Base: 2 5 2 2 2 c ---[ 8]---> BDD-cost: 76 c ---[ 7]---> Sorter-cost: 2550 Base: 2 5 2 2 2 c ---[ 6]---> Adder-cost: 223 maxlim: 249 bits: 9/8 c ---[ 5]---> BDD-cost: 48 c ---[ 4]---> BDD-cost: 114 c ---[ 3]---> BDD-cost: 55 c ---[ 2]---> Sorter-cost: 2935 Base: 2 5 2 2 2 2 c ---[ 1]---> Adder-cost: 212 maxlim: 230 bits: 9/8 c ---[ 0]---> BDD-cost: 92 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 30742 79537 | 10247 0 0 nan | 0.000 % | c | 100 | 30742 79537 | 11271 100 544 5.4 | 0.987 % | c | 250 | 30742 79537 | 12398 250 2459 9.8 | 0.986 % | c | 477 | 30742 79537 | 13638 477 3973 8.3 | 0.986 % | c ============================================================================== c [1mFound solution: 175459[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:92424 Base: 2 2 2 3 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 | 637 | 284458 671673 | 94819 637 11349 17.8 | 0.986 % | c | 737 | 284437 671627 | 104300 735 12835 17.5 | 0.117 % | c | 887 | 284035 670723 | 114730 880 13845 15.7 | 0.221 % | c | 1114 | 284035 670723 | 126204 1107 15250 13.8 | 0.221 % | c | 1451 | 284035 670723 | 138824 1444 17597 12.2 | 0.221 % | c | 1958 | 282828 667995 | 152706 1939 63559 32.8 | 0.549 % | c | 2717 | 282661 667617 | 167977 2697 148878 55.2 | 0.596 % | c | 3856 | 271841 642801 | 184775 3781 190178 50.3 | 3.911 % | c | 5565 | 267485 632765 | 203252 5455 244772 44.9 | 5.294 % | c | 8129 | 258374 611785 | 223578 7920 366516 46.3 | 8.175 % | c | 11974 | 255958 606212 | 245936 11748 726453 61.8 | 8.939 % | c | 17740 | 250695 594032 | 270529 17444 1194291 68.5 | 10.666 % | c | 26390 | 249167 590517 | 297582 26068 1851301 71.0 | 11.165 % | c | 39364 | 243608 577673 | 327340 38951 2440127 62.6 | 12.969 % | c ============================================================================== c [1mFound solution: 174126[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:70620 Base: 2 2 2 3 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 | 57904 | 404098 950841 | 134699 57401 4098734 71.4 | 12.969 % | c | 58008 | 403639 949827 | 148168 57502 4100867 71.3 | 14.245 % | c | 58159 | 402994 948375 | 162985 57644 4103732 71.2 | 14.375 % | c | 58384 | 402994 948375 | 179284 57869 4109174 71.0 | 14.375 % | c | 58721 | 401268 944466 | 197212 58185 4111678 70.7 | 14.715 % | c | 59229 | 401268 944466 | 216934 58693 4136023 70.5 | 14.715 % | c | 59988 | 401268 944466 | 238627 59452 4283010 72.0 | 14.715 % | c | 61127 | 401110 944098 | 262490 60582 4296313 70.9 | 14.748 % | c | 62836 | 400965 943764 | 288739 62290 4391753 70.5 | 14.776 % | c | 65398 | 397076 934924 | 317613 64748 4501421 69.5 | 15.543 % | c | 69242 | 396305 933196 | 349374 68585 4939320 72.0 | 15.693 % | c ============================================================================== c [1mFound solution: 172189[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:69141 Base: 2 2 2 3 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 | 73398 | 544035 1277084 | 181345 72562 5065701 69.8 | 15.693 % | c | 73498 | 544035 1277084 | 199479 72662 5068684 69.8 | 16.507 % | c | 73648 | 544035 1277084 | 219427 72812 5070213 69.6 | 16.507 % | c | 73873 | 543068 1274852 | 241370 72952 5097260 69.9 | 16.641 % | c | 74210 | 540987 1270145 | 265507 73257 5099628 69.6 | 16.928 % | c | 74716 | 540190 1268331 | 292057 73706 5103053 69.2 | 17.043 % | c | 75475 | 536077 1259024 | 321263 74187 5111911 68.9 | 17.612 % | c | 76614 | 536077 1259024 | 353390 75326 5156748 68.5 | 17.612 % | c | 78323 | 530933 1247267 | 388729 76556 5221852 68.2 | 18.328 % | c ============================================================================== c [1mFound solution: 165654[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 3 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 | 78741 | 531464 1248864 | 177154 76974 5254301 68.3 | 18.328 % | c | 78842 | 530814 1247415 | 194869 77072 5256580 68.2 | 18.396 % | c | 78994 | 530399 1246465 | 214356 77218 5264119 68.2 | 18.455 % | c | 79219 | 530399 1246465 | 235791 77443 5280849 68.2 | 18.455 % | c | 79556 | 530293 1246228 | 259371 77779 5290167 68.0 | 18.466 % | c | 80062 | 530239 1246109 | 285308 78283 5319511 68.0 | 18.473 % | c | 80821 | 530239 1246109 | 313839 79042 5399819 68.3 | 18.473 % | c | 81960 | 530034 1245656 | 345223 80180 5665661 70.7 | 18.500 % | c | 83669 | 524072 1232048 | 379745 81399 5764458 70.8 | 19.341 % | c | 86231 | 522340 1228063 | 417719 83937 5900609 70.3 | 19.584 % | c ============================================================================== c [1mFound solution: 165192[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:68242 Base: 2 2 2 3 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 | 87232 | 675287 1583479 | 225095 84938 6115837 72.0 | 19.584 % | c | 87332 | 675287 1583479 | 247604 85038 6117351 71.9 | 19.030 % | c | 87483 | 673704 1579889 | 272364 85180 6121380 71.9 | 19.205 % | c | 87709 | 673704 1579889 | 299601 85406 6147900 72.0 | 19.205 % | c | 88046 | 673704 1579889 | 329561 85743 6190662 72.2 | 19.205 % | c | 88553 | 673704 1579889 | 362517 86250 6204900 71.9 | 19.205 % | c | 89314 | 673704 1579889 | 398769 87011 6265601 72.0 | 19.205 % | c | 90456 | 668664 1568463 | 438646 88034 6376824 72.4 | 19.756 % | c | 92164 | 666346 1563278 | 482511 89724 6660716 74.2 | 20.003 % | c | 94726 | 666346 1563278 | 530762 92286 7009786 76.0 | 20.003 % | c | 98570 | 664362 1558830 | 583838 96127 7652673 79.6 | 20.223 % | c ============================================================================== c [1mFound solution: 164617[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 3 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 | 98680 | 664408 1559385 | 221469 96237 7659605 79.6 | 20.223 % | c | 98781 | 664408 1559385 | 243615 96338 7666260 79.6 | 20.222 % | c | 98931 | 663882 1558213 | 267977 96478 7669094 79.5 | 20.280 % | c | 99156 | 663882 1558213 | 294775 96703 7674639 79.4 | 20.280 % | c | 99494 | 663882 1558213 | 324252 97041 7682075 79.2 | 20.280 % | c | 100000 | 662711 1555549 | 356678 97537 7702428 79.0 | 20.411 % | c | 100761 | 658022 1544826 | 392345 98090 7724938 78.8 | 20.924 % | c | 101902 | 657896 1544545 | 431580 99228 7828742 78.9 | 20.939 % | c | 103612 | 656006 1540264 | 474738 100809 7919978 78.6 | 21.151 % | c | 106174 | 653447 1534433 | 522212 103311 8338281 80.7 | 21.441 % | c | 110018 | 653447 1534433 | 574433 107155 8992194 83.9 | 21.441 % | c | 115784 | 650518 1527749 | 631876 112772 9214928 81.7 | 21.761 % | c | 124433 | 650518 1527749 | 695064 121421 9889029 81.4 | 21.761 % | c ============================================================================== c [1mFound solution: 163483[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 3 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 | 131430 | 646191 1517922 | 215397 128336 10361434 80.7 | 21.761 % | c | 131530 | 646191 1517922 | 236936 128436 10366789 80.7 | 22.242 % | c | 131680 | 646026 1517552 | 260630 128583 10382200 80.7 | 22.260 % | c | 131906 | 646026 1517552 | 286693 128809 10384118 80.6 | 22.260 % | c | 132243 | 646026 1517552 | 315362 129146 10387012 80.4 | 22.260 % | c | 132750 | 645201 1515676 | 346899 129631 10391486 80.2 | 22.349 % | c | 133510 | 642926 1510464 | 381588 130236 10419037 80.0 | 22.602 % | c | 134650 | 642926 1510464 | 419747 131376 10465729 79.7 | 22.602 % | c ============================================================================== c [1mFound solution: 161824[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 3 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 | 135225 | 642822 1510228 | 214274 131950 10510329 79.7 | 22.602 % | c | 135328 | 642822 1510228 | 235701 132053 10515914 79.6 | 22.614 % | c | 135478 | 642047 1508455 | 259271 132190 10518344 79.6 | 22.694 % | c | 135703 | 642047 1508455 | 285198 132415 10522658 79.5 | 22.694 % | c | 136040 | 641491 1507180 | 313718 132743 10524190 79.3 | 22.755 % | c | 136547 | 641393 1506955 | 345090 133249 10584627 79.4 | 22.766 % | c | 137306 | 641201 1506523 | 379599 134000 10677526 79.7 | 22.785 % | c | 138445 | 640805 1505618 | 417559 135124 10695361 79.2 | 22.828 % | c | 140154 | 637215 1497411 | 459315 136401 10708038 78.5 | 23.224 % | c c *** TERMINATED *** s SATISFIABLE v -x_0x2e__0x2e__0x2e_0101_bit0 -x_0x2e__0x2e__0x2e_0101_bit1 -x_0x2e__0x2e__0x2e_0101_bit2 -x_0x2e__0x2e__0x2e_0101_bit3 -x_0x2e__0x2e__0x2e_0201_bit0 -x_0x2e__0x2e__0x2e_0201_bit1 -x_0x2e__0x2e__0x2e_0201_bit2 -x_0x2e__0x2e__0x2e_0201_bit3 -x_0x2e__0x2e__0x2e_0301_bit0 -x_0x2e__0x2e__0x2e_0301_bit1 x_0x2e__0x2e__0x2e_0301_bit2 -x_0x2e__0x2e__0x2e_0301_bit3 -x_0x2e__0x2e__0x2e_0401_bit0 -x_0x2e__0x2e__0x2e_0401_bit1 -x_0x2e__0x2e__0x2e_0401_bit2 -x_0x2e__0x2e__0x2e_0401_bit3 -x_0x2e__0x2e__0x2e_0701_bit0 -x_0x2e__0x2e__0x2e_0701_bit1 -x_0x2e__0x2e__0x2e_0701_bit2 -x_0x2e__0x2e__0x2e_0701_bit3 -x_0x2e__0x2e__0x2e_0801_bit0 -x_0x2e__0x2e__0x2e_0801_bit1 -x_0x2e__0x2e__0x2e_0801_bit2 -x_0x2e__0x2e__0x2e_0801_bit3 x_0x2e__0x2e__0x2e_0901_bit0 -x_0x2e__0x2e__0x2e_0901_bit1 x_0x2e__0x2e__0x2e_0901_bit2 -x_0x2e__0x2e__0x2e_0901_bit3 -x_0x2e__0x2e__0x2e_1001_bit0 -x_0x2e__0x2e__0x2e_1001_bit1 -x_0x2e__0x2e__0x2e_1001_bit2 -x_0x2e__0x2e__0x2e_1001_bit3 -x_0x2e__0x2e__0x2e_0102_bit0 -x_0x2e__0x2e__0x2e_0102_bit1 -x_0x2e__0x2e__0x2e_0102_bit2 -x_0x2e__0x2e__0x2e_0102_bit3 -x_0x2e__0x2e__0x2e_0202_bit0 -x_0x2e__0x2e__0x2e_0202_bit1 -x_0x2e__0x2e__0x2e_0202_bit2 -x_0x2e__0x2e__0x2e_0202_bit3 -x_0x2e__0x2e__0x2e_0302_bit0 -x_0x2e__0x2e__0x2e_0302_bit1 -x_0x2e__0x2e__0x2e_0302_bit2 x_0x2e__0x2e__0x2e_0302_bit3 -x_0x2e__0x2e__0x2e_0402_bit0 -x_0x2e__0x2e__0x2e_0402_bit1 -x_0x2e__0x2e__0x2e_0402_bit2 -x_0x2e__0x2e__0x2e_0402_bit3 -x_0x2e__0x2e__0x2e_0502_bit0 -x_0x2e__0x2e__0x2e_0502_bit1 x_0x2e__0x2e__0x2e_0502_bit2 -x_0x2e__0x2e__0x2e_0502_bit3 -x_0x2e__0x2e__0x2e_0602_bit0 -x_0x2e__0x2e__0x2e_0602_bit1 -x_0x2e__0x2e__0x2e_0602_bit2 -x_0x2e__0x2e__0x2e_0602_bit3 -x_0x2e__0x2e__0x2e_0702_bit0 -x_0x2e__0x2e__0x2e_0702_bit1 -x_0x2e__0x2e__0x2e_0702_bit2 -x_0x2e__0x2e__0x2e_0702_bit3 -x_0x2e__0x2e__0x2e_0802_bit0 -x_0x2e__0x2e__0x2e_0802_bit1 -x_0x2e__0x2e__0x2e_0802_bit2 -x_0x2e__0x2e__0x2e_0802_bit3 -x_0x2e__0x2e__0x2e_0902_bit0 -x_0x2e__0x2e__0x2e_0902_bit1 -x_0x2e__0x2e__0x2e_0902_bit2 -x_0x2e__0x2e__0x2e_0902_bit3 -x_0x2e__0x2e__0x2e_1002_bit0 -x_0x2e__0x2e__0x2e_1002_bit1 -x_0x2e__0x2e__0x2e_1002_bit2 -x_0x2e__0x2e__0x2e_1002_bit3 -x_0x2e__0x2e__0x2e_1102_bit0 x_0x2e__0x2e__0x2e_1102_bit1 -x_0x2e__0x2e__0x2e_1102_bit2 -x_0x2e__0x2e__0x2e_1102_bit3 -x_0x2e__0x2e__0x2e_1202_bit0 -x_0x2e__0x2e__0x2e_1202_bit1 -x_0x2e__0x2e__0x2e_1202_bit2 -x_0x2e__0x2e__0x2e_1202_bit3 x_0x2e__0x2e__0x2e_0103_bit0 -x_0x2e__0x2e__0x2e_0103_bit1 -x_0x2e__0x2e__0x2e_0103_bit2 -x_0x2e__0x2e__0x2e_0103_bit3 x_0x2e__0x2e__0x2e_0203_bit0 -x_0x2e__0x2e__0x2e_0203_bit1 x_0x2e__0x2e__0x2e_0203_bit2 -x_0x2e__0x2e__0x2e_0203_bit3 -x_0x2e__0x2e__0x2e_0303_bit0 x_0x2e__0x2e__0x2e_0303_bit1 -x_0x2e__0x2e__0x2e_0303_bit2 -x_0x2e__0x2e__0x2e_0303_bit3 x_0x2e__0x2e__0x2e_0403_bit0 -x_0x2e__0x2e__0x2e_0403_bit1 -x_0x2e__0x2e__0x2e_0403_bit2 -x_0x2e__0x2e__0x2e_0403_bit3 -x_0x2e__0x2e__0x2e_0503_bit0 -x_0x2e__0x2e__0x2e_0503_bit1 -x_0x2e__0x2e__0x2e_0503_bit2 -x_0x2e__0x2e__0x2e_0503_bit3 -x_0x2e__0x2e__0x2e_0603_bit0 -x_0x2e__0x2e__0x2e_0603_bit1 -x_0x2e__0x2e__0x2e_0603_bit2 -x_0x2e__0x2e__0x2e_0603_bit3 x_0x2e__0x2e__0x2e_0703_bit0 -x_0x2e__0x2e__0x2e_0703_bit1 -x_0x2e__0x2e__0x2e_0703_bit2 -x_0x2e__0x2e__0x2e_0703_bit3 x_0x2e__0x2e__0x2e_0803_bit0 -x_0x2e__0x2e__0x2e_0803_bit1 -x_0x2e__0x2e__0x2e_0803_bit2 -x_0x2e__0x2e__0x2e_0803_bit3 -x_0x2e__0x2e__0x2e_0903_bit0 x_0x2e__0x2e__0x2e_0903_bit1 -x_0x2e__0x2e__0x2e_0903_bit2 -x_0x2e__0x2e__0x2e_0903_bit3 x_0x2e__0x2e__0x2e_1003_bit0 -x_0x2e__0x2e__0x2e_1003_bit1 -x_0x2e__0x2e__0x2e_1003_bit2 -x_0x2e__0x2e__0x2e_1003_bit3 -x_0x2e__0x2e__0x2e_1103_bit0 -x_0x2e__0x2e__0x2e_1103_bit1 -x_0x2e__0x2e__0x2e_1103_bit2 -x_0x2e__0x2e__0x2e_1103_bit3 -x_0x2e__0x2e__0x2e_1203_bit0 -x_0x2e__0x2e__0x2e_1203_bit1 -x_0x2e__0x2e__0x2e_1203_bit2 -x_0x2e__0x2e__0x2e_1203_bit3 -x_0x2e__0x2e__0x2e_0104_bit0 -x_0x2e__0x2e__0x2e_0204_bit0 -x_0x2e__0x2e__0x2e_0304_bit0 -x_0x2e__0x2e__0x2e_0404_bit0 -x_0x2e__0x2e__0x2e_0504_bit0 -x_0x2e__0x2e__0x2e_0604_bit0 -x_0x2e__0x2e__0x2e_0704_bit0 -x_0x2e__0x2e__0x2e_0804_bit0 -x_0x2e__0x2e__0x2e_0904_bit0 -x_0x2e__0x2e__0x2e_1004_bit0 -x_0x2e__0x2e__0x2e_1104_bit0 x_0x2e__0x2e__0x2e_1204_bit0 -x_0x2e__0x2e__0x2e_0105_bit0 -x_0x2e__0x2e__0x2e_0105_bit1 -x_0x2e__0x2e__0x2e_0105_bit2 -x_0x2e__0x2e__0x2e_0205_bit0 -x_0x2e__0x2e__0x2e_0205_bit1 -x_0x2e__0x2e__0x2e_0205_bit2 -x_0x2e__0x2e__0x2e_0305_bit0 -x_0x2e__0x2e__0x2e_0305_bit1 -x_0x2e__0x2e__0x2e_0305_bit2 -x_0x2e__0x2e__0x2e_0405_bit0 -x_0x2e__0x2e__0x2e_0405_bit1 -x_0x2e__0x2e__0x2e_0405_bit2 x_0x2e__0x2e__0x2e_0505_bit0 -x_0x2e__0x2e__0x2e_0505_bit1 -x_0x2e__0x2e__0x2e_0505_bit2 x_0x2e__0x2e__0x2e_0605_bit0 -x_0x2e__0x2e__0x2e_0605_bit1 -x_0x2e__0x2e__0x2e_0605_bit2 -x_0x2e__0x2e__0x2e_0705_bit0 -x_0x2e__0x2e__0x2e_0705_bit1 -x_0x2e__0x2e__0x2e_0705_bit2 -x_0x2e__0x2e__0x2e_0805_bit0 -x_0x2e__0x2e__0x2e_0805_bit1 -x_0x2e__0x2e__0x2e_0805_bit2 -x_0x2e__0x2e__0x2e_0905_bit0 -x_0x2e__0x2e__0x2e_0905_bit1 -x_0x2e__0x2e__0x2e_0905_bit2 -x_0x2e__0x2e__0x2e_1005_bit0 -x_0x2e__0x2e__0x2e_1005_bit1 -x_0x2e__0x2e__0x2e_1005_bit2 x_0x2e__0x2e__0x2e_1105_bit0 -x_0x2e__0x2e__0x2e_1105_bit1 -x_0x2e__0x2e__0x2e_1105_bit2 x_0x2e__0x2e__0x2e_1205_bit0 -x_0x2e__0x2e__0x2e_1205_bit1 -x_0x2e__0x2e__0x2e_1205_bit2 -x_0x2e__0x2e__0x2e_0106_bit0 -x_0x2e__0x2e__0x2e_0106_bit1 -x_0x2e__0x2e__0x2e_0106_bit2 -x_0x2e__0x2e__0x2e_0106_bit3 -x_0x2e__0x2e__0x2e_0206_bit0 -x_0x2e__0x2e__0x2e_0206_bit1 -x_0x2e__0x2e__0x2e_0206_bit2 -x_0x2e__0x2e__0x2e_0206_bit3 -x_0x2e__0x2e__0x2e_0306_bit0 -x_0x2e__0x2e__0x2e_0306_bit1 x_0x2e__0x2e__0x2e_0306_bit2 -x_0x2e__0x2e__0x2e_0306_bit3 -x_0x2e__0x2e__0x2e_0406_bit0 -x_0x2e__0x2e__0x2e_0406_bit1 -x_0x2e__0x2e__0x2e_0406_bit2 -x_0x2e__0x2e__0x2e_0406_bit3 -x_0x2e__0x2e__0x2e_0506_bit0 -x_0x2e__0x2e__0x2e_0506_bit1 -x_0x2e__0x2e__0x2e_0506_bit2 -x_0x2e__0x2e__0x2e_0506_bit3 -x_0x2e__0x2e__0x2e_0606_bit0 -x_0x2e__0x2e__0x2e_0606_bit1 -x_0x2e__0x2e__0x2e_0606_bit2 -x_0x2e__0x2e__0x2e_0606_bit3 -x_0x2e__0x2e__0x2e_0706_bit0 -x_0x2e__0x2e__0x2e_0706_bit1 -x_0x2e__0x2e__0x2e_0706_bit2 -x_0x2e__0x2e__0x2e_0706_bit3 -x_0x2e__0x2e__0x2e_0806_bit0 -x_0x2e__0x2e__0x2e_0806_bit1 -x_0x2e__0x2e__0x2e_0806_bit2 -x_0x2e__0x2e__0x2e_0806_bit3 -x_0x2e__0x2e__0x2e_0906_bit0 -x_0x2e__0x2e__0x2e_0906_bit1 x_0x2e__0x2e__0x2e_0906_bit2 -x_0x2e__0x2e__0x2e_0906_bit3 -x_0x2e__0x2e__0x2e_1006_bit0 -x_0x2e__0x2e__0x2e_1006_bit1 -x_0x2e__0x2e__0x2e_1006_bit2 -x_0x2e__0x2e__0x2e_1006_bit3 -x_0x2e__0x2e__0x2e_1106_bit0 -x_0x2e__0x2e__0x2e_1106_bit1 -x_0x2e__0x2e__0x2e_1106_bit2 -x_0x2e__0x2e__0x2e_1106_bit3 -x_0x2e__0x2e__0x2e_1206_bit0 -x_0x2e__0x2e__0x2e_1206_bit1 -x_0x2e__0x2e__0x2e_1206_bit2 -x_0x2e__0x2e__0x2e_1206_bit3 x_0x2e__0x2e__0x2e_0507_bit0 -x_0x2e__0x2e__0x2e_0507_bit1 -x_0x2e__0x2e__0x2e_0507_bit2 x_0x2e__0x2e__0x2e_0607_bit0 -x_0x2e__0x2e__0x2e_0607_bit1 -x_0x2e__0x2e__0x2e_0607_bit2 x_0x2e__0x2e__0x2e_1107_bit0 -x_0x2e__0x2e__0x2e_1107_bit1 -x_0x2e__0x2e__0x2e_1107_bit2 x_0x2e__0x2e__0x2e_1207_bit0 -x_0x2e__0x2e__0x2e_1207_bit1 -x_0x2e__0x2e__0x2e_1207_bit2 -x_0x2e__0x2e__0x2e_0108_bit0 -x_0x2e__0x2e__0x2e_0108_bit1 -x_0x2e__0x2e__0x2e_0108_bit2 -x_0x2e__0x2e__0x2e_0108_bit3 -x_0x2e__0x2e__0x2e_0208_bit0 -x_0x2e__0x2e__0x2e_0208_bit1 -x_0x2e__0x2e__0x2e_0208_bit2 -x_0x2e__0x2e__0x2e_0208_bit3 -x_0x2e__0x2e__0x2e_0308_bit0 x_0x2e__0x2e__0x2e_0308_bit1 -x_0x2e__0x2e__0x2e_0308_bit2 x_0x2e__0x2e__0x2e_0308_bit3 -x_0x2e__0x2e__0x2e_0408_bit0 -x_0x2e__0x2e__0x2e_0408_bit1 -x_0x2e__0x2e__0x2e_0408_bit2 -x_0x2e__0x2e__0x2e_0408_bit3 -x_0x2e__0x2e__0x2e_0708_bit0 -x_0x2e__0x2e__0x2e_0708_bit1 -x_0x2e__0x2e__0x2e_0708_bit2 -x_0x2e__0x2e__0x2e_0708_bit3 -x_0x2e__0x2e__0x2e_0808_bit0 -x_0x2e__0x2e__0x2e_0808_bit1 -x_0x2e__0x2e__0x2e_0808_bit2 -x_0x2e__0x2e__0x2e_0808_bit3 -x_0x2e__0x2e__0x2e_0908_bit0 x_0x2e__0x2e__0x2e_0908_bit1 -x_0x2e__0x2e__0x2e_0908_bit2 -x_0x2e__0x2e__0x2e_0908_bit3 -x_0x2e__0x2e__0x2e_1008_bit0 -x_0x2e__0x2e__0x2e_1008_bit1 -x_0x2e__0x2e__0x2e_1008_bit2 -x_0x2e__0x2e__0x2e_1008_bit3 -x_0x2e__0x2e__0x2e_0109_bit0 -x_0x2e__0x2e__0x2e_0109_bit1 -x_0x2e__0x2e__0x2e_0109_bit2 -x_0x2e__0x2e__0x2e_0209_bit0 -x_0x2e__0x2e__0x2e_0209_bit1 -x_0x2e__0x2e__0x2e_0209_bit2 -x_0x2e__0x2e__0x2e_0309_bit0 -x_0x2e__0x2e__0x2e_0309_bit1 -x_0x2e__0x2e__0x2e_0309_bit2 -x_0x2e__0x2e__0x2e_0409_bit0 -x_0x2e__0x2e__0x2e_0409_bit1 -x_0x2e__0x2e__0x2e_0409_bit2 -x_0x2e__0x2e__0x2e_0509_bit0 -x_0x2e__0x2e__0x2e_0509_bit1 -x_0x2e__0x2e__0x2e_0509_bit2 x_0x2e__0x2e__0x2e_0609_bit0 x_0x2e__0x2e__0x2e_0609_bit1 -x_0x2e__0x2e__0x2e_0609_bit2 -x_0x2e__0x2e__0x2e_0709_bit0 -x_0x2e__0x2e__0x2e_0709_bit1 -x_0x2e__0x2e__0x2e_0709_bit2 x_0x2e__0x2e__0x2e_0809_bit0 -x_0x2e__0x2e__0x2e_0809_bit1 -x_0x2e__0x2e__0x2e_0809_bit2 -x_0x2e__0x2e__0x2e_0909_bit0 -x_0x2e__0x2e__0x2e_0909_bit1 -x_0x2e__0x2e__0x2e_0909_bit2 x_0x2e__0x2e__0x2e_1009_bit0 -x_0x2e__0x2e__0x2e_1009_bit1 -x_0x2e__0x2e__0x2e_1009_bit2 -x_0x2e__0x2e__0x2e_1109_bit0 -x_0x2e__0x2e__0x2e_1109_bit1 -x_0x2e__0x2e__0x2e_1109_bit2 -x_0x2e__0x2e__0x2e_1209_bit0 -x_0x2e__0x2e__0x2e_1209_bit1 -x_0x2e__0x2e__0x2e_1209_bit2 -x_0x2e__0x2e__0x2e_0110_bit0 -x_0x2e__0x2e__0x2e_0110_bit1 x_0x2e__0x2e__0x2e_0110_bit2 -x_0x2e__0x2e__0x2e_0111_bit0 -x_0x2e__0x2e__0x2e_0111_bit1 -x_0x2e__0x2e__0x2e_0111_bit2 -x_0x2e__0x2e__0x2e_0112_bit0 -x_0x2e__0x2e__0x2e_0112_bit1 -x_0x2e__0x2e__0x2e_0112_bit2 -x_0x2e__0x2e__0x2e_0112_bit3 x_0x2e__0x2e__0x2e_0113_bit0 -x_0x2e__0x2e__0x2e_0113_bit1 -x_0x2e__0x2e__0x2e_0113_bit2 -x_0x2e__0x2e__0x2e_0114_bit0 -x_0x2e__0x2e__0x2e_0114_bit1 -x_0x2e__0x2e__0x2e_0114_bit2 -x_0x2e__0x2e__0x2e_0115_bit0 x_0x2e__0x2e__0x2e_0115_bit1 x_0x2e__0x2e__0x2e_0116_bit0 -x_0x2e__0x2e__0x2e_0116_bit1 -x_0x2e__0x2e__0x2e_0117_bit0 -x_0x2e__0x2e__0x2e_0210_bit0 -x_0x2e__0x2e__0x2e_0210_bit1 -x_0x2e__0x2e__0x2e_0210_bit2 -x_0x2e__0x2e__0x2e_0211_bit0 -x_0x2e__0x2e__0x2e_0211_bit1 -x_0x2e__0x2e__0x2e_0211_bit2 -x_0x2e__0x2e__0x2e_0212_bit0 -x_0x2e__0x2e__0x2e_0212_bit1 -x_0x2e__0x2e__0x2e_0212_bit2 -x_0x2e__0x2e__0x2e_0212_bit3 -x_0x2e__0x2e__0x2e_0213_bit0 -x_0x2e__0x2e__0x2e_0213_bit1 -x_0x2e__0x2e__0x2e_0213_bit2 -x_0x2e__0x2e__0x2e_0214_bit0 -x_0x2e__0x2e__0x2e_0214_bit1 -x_0x2e__0x2e__0x2e_0214_bit2 -x_0x2e__0x2e__0x2e_0215_bit0 -x_0x2e__0x2e__0x2e_0215_bit1 -x_0x2e__0x2e__0x2e_0216_bit0 -x_0x2e__0x2e__0x2e_0216_bit1 -x_0x2e__0x2e__0x2e_0217_bit0 -x_0x2e__0x2e__0x2e_0310_bit0 -x_0x2e__0x2e__0x2e_0310_bit1 -x_0x2e__0x2e__0x2e_0310_bit2 -x_0x2e__0x2e__0x2e_0311_bit0 -x_0x2e__0x2e__0x2e_0311_bit1 -x_0x2e__0x2e__0x2e_0311_bit2 -x_0x2e__0x2e__0x2e_0312_bit0 -x_0x2e__0x2e__0x2e_0312_bit1 -x_0x2e__0x2e__0x2e_0312_bit2 -x_0x2e__0x2e__0x2e_0312_bit3 -x_0x2e__0x2e__0x2e_0313_bit0 -x_0x2e__0x2e__0x2e_0313_bit1 -x_0x2e__0x2e__0x2e_0313_bit2 -x_0x2e__0x2e__0x2e_0314_bit0 -x_0x2e__0x2e__0x2e_0314_bit1 -x_0x2e__0x2e__0x2e_0314_bit2 -x_0x2e__0x2e__0x2e_0315_bit0 -x_0x2e__0x2e__0x2e_0315_bit1 -x_0x2e__0x2e__0x2e_0316_bit0 -x_0x2e__0x2e__0x2e_0316_bit1 -x_0x2e__0x2e__0x2e_0317_bit0 -x_0x2e__0x2e__0x2e_0410_bit0 -x_0x2e__0x2e__0x2e_0410_bit1 -x_0x2e__0x2e__0x2e_0410_bit2 -x_0x2e__0x2e__0x2e_0411_bit0 -x_0x2e__0x2e__0x2e_0411_bit1 -x_0x2e__0x2e__0x2e_0411_bit2 -x_0x2e__0x2e__0x2e_0412_bit0 -x_0x2e__0x2e__0x2e_0412_bit1 -x_0x2e__0x2e__0x2e_0412_bit2 x_0x2e__0x2e__0x2e_0412_bit3 -x_0x2e__0x2e__0x2e_0413_bit0 -x_0x2e__0x2e__0x2e_0413_bit1 -x_0x2e__0x2e__0x2e_0413_bit2 -x_0x2e__0x2e__0x2e_0414_bit0 -x_0x2e__0x2e__0x2e_0414_bit1 -x_0x2e__0x2e__0x2e_0414_bit2 -x_0x2e__0x2e__0x2e_0415_bit0 -x_0x2e__0x2e__0x2e_0415_bit1 -x_0x2e__0x2e__0x2e_0416_bit0 -x_0x2e__0x2e__0x2e_0416_bit1 -x_0x2e__0x2e__0x2e_0417_bit0 -x_0x2e__0x2e__0x2e_0510_bit0 -x_0x2e__0x2e__0x2e_0510_bit1 -x_0x2e__0x2e__0x2e_0510_bit2 -x_0x2e__0x2e__0x2e_0511_bit0 -x_0x2e__0x2e__0x2e_0511_bit1 -x_0x2e__0x2e__0x2e_0511_bit2 -x_0x2e__0x2e__0x2e_0512_bit0 -x_0x2e__0x2e__0x2e_0512_bit1 -x_0x2e__0x2e__0x2e_0512_bit2 -x_0x2e__0x2e__0x2e_0512_bit3 -x_0x2e__0x2e__0x2e_0513_bit0 -x_0x2e__0x2e__0x2e_0513_bit1 -x_0x2e__0x2e__0x2e_0513_bit2 -x_0x2e__0x2e__0x2e_0514_bit0 -x_0x2e__0x2e__0x2e_0514_bit1 -x_0x2e__0x2e__0x2e_0514_bit2 -x_0x2e__0x2e__0x2e_0515_bit0 -x_0x2e__0x2e__0x2e_0515_bit1 -x_0x2e__0x2e__0x2e_0516_bit0 -x_0x2e__0x2e__0x2e_0516_bit1 -x_0x2e__0x2e__0x2e_0517_bit0 -x_0x2e__0x2e__0x2e_0610_bit0 -x_0x2e__0x2e__0x2e_0610_bit1 -x_0x2e__0x2e__0x2e_0610_bit2 -x_0x2e__0x2e__0x2e_0611_bit0 -x_0x2e__0x2e__0x2e_0611_bit1 -x_0x2e__0x2e__0x2e_0611_bit2 -x_0x2e__0x2e__0x2e_0612_bit0 -x_0x2e__0x2e__0x2e_0612_bit1 -x_0x2e__0x2e__0x2e_0612_bit2 -x_0x2e__0x2e__0x2e_0612_bit3 -x_0x2e__0x2e__0x2e_0613_bit0 -x_0x2e__0x2e__0x2e_0613_bit1 -x_0x2e__0x2e__0x2e_0613_bit2 -x_0x2e__0x2e__0x2e_0614_bit0 -x_0x2e__0x2e__0x2e_0614_bit1 -x_0x2e__0x2e__0x2e_0614_bit2 -x_0x2e__0x2e__0x2e_0615_bit0 -x_0x2e__0x2e__0x2e_0615_bit1 -x_0x2e__0x2e__0x2e_0616_bit0 -x_0x2e__0x2e__0x2e_0616_bit1 -x_0x2e__0x2e__0x2e_0617_bit0 -x_0x2e__0x2e__0x2e_0710_bit0 -x_0x2e__0x2e__0x2e_0710_bit1 -x_0x2e__0x2e__0x2e_0710_bit2 -x_0x2e__0x2e__0x2e_0711_bit0 -x_0x2e__0x2e__0x2e_0711_bit1 -x_0x2e__0x2e__0x2e_0711_bit2 -x_0x2e__0x2e__0x2e_0712_bit0 -x_0x2e__0x2e__0x2e_0712_bit1 -x_0x2e__0x2e__0x2e_0712_bit2 -x_0x2e__0x2e__0x2e_0712_bit3 x_0x2e__0x2e__0x2e_0713_bit0 -x_0x2e__0x2e__0x2e_0713_bit1 -x_0x2e__0x2e__0x2e_0713_bit2 -x_0x2e__0x2e__0x2e_0714_bit0 x_0x2e__0x2e__0x2e_0714_bit1 -x_0x2e__0x2e__0x2e_0714_bit2 -x_0x2e__0x2e__0x2e_0715_bit0 -x_0x2e__0x2e__0x2e_0715_bit1 -x_0x2e__0x2e__0x2e_0716_bit0 -x_0x2e__0x2e__0x2e_0716_bit1 -x_0x2e__0x2e__0x2e_0717_bit0 -x_0x2e__0x2e__0x2e_0810_bit0 -x_0x2e__0x2e__0x2e_0810_bit1 -x_0x2e__0x2e__0x2e_0810_bit2 -x_0x2e__0x2e__0x2e_0811_bit0 -x_0x2e__0x2e__0x2e_0811_bit1 -x_0x2e__0x2e__0x2e_0811_bit2 -x_0x2e__0x2e__0x2e_0812_bit0 -x_0x2e__0x2e__0x2e_0812_bit1 -x_0x2e__0x2e__0x2e_0812_bit2 -x_0x2e__0x2e__0x2e_0812_bit3 -x_0x2e__0x2e__0x2e_0813_bit0 -x_0x2e__0x2e__0x2e_0813_bit1 -x_0x2e__0x2e__0x2e_0813_bit2 -x_0x2e__0x2e__0x2e_0814_bit0 -x_0x2e__0x2e__0x2e_0814_bit1 -x_0x2e__0x2e__0x2e_0814_bit2 -x_0x2e__0x2e__0x2e_0815_bit0 -x_0x2e__0x2e__0x2e_0815_bit1 -x_0x2e__0x2e__0x2e_0816_bit0 -x_0x2e__0x2e__0x2e_0816_bit1 -x_0x2e__0x2e__0x2e_0817_bit0 x_0x2e__0x2e__0x2e_0910_bit0 -x_0x2e__0x2e__0x2e_0910_bit1 -x_0x2e__0x2e__0x2e_0910_bit2 -x_0x2e__0x2e__0x2e_0911_bit0 -x_0x2e__0x2e__0x2e_0911_bit1 x_0x2e__0x2e__0x2e_0911_bit2 -x_0x2e__0x2e__0x2e_0912_bit0 -x_0x2e__0x2e__0x2e_0912_bit1 -x_0x2e__0x2e__0x2e_0912_bit2 -x_0x2e__0x2e__0x2e_0912_bit3 x_0x2e__0x2e__0x2e_0913_bit0 -x_0x2e__0x2e__0x2e_0913_bit1 -x_0x2e__0x2e__0x2e_0913_bit2 x_0x2e__0x2e__0x2e_0914_bit0 -x_0x2e__0x2e__0x2e_0914_bit1 -x_0x2e__0x2e__0x2e_0914_bit2 -x_0x2e__0x2e__0x2e_0915_bit0 -x_0x2e__0x2e__0x2e_0915_bit1 -x_0x2e__0x2e__0x2e_0916_bit0 -x_0x2e__0x2e__0x2e_0916_bit1 -x_0x2e__0x2e__0x2e_0917_bit0 -x_0x2e__0x2e__0x2e_1010_bit0 -x_0x2e__0x2e__0x2e_1010_bit1 -x_0x2e__0x2e__0x2e_1010_bit2 -x_0x2e__0x2e__0x2e_1011_bit0 -x_0x2e__0x2e__0x2e_1011_bit1 -x_0x2e__0x2e__0x2e_1011_bit2 -x_0x2e__0x2e__0x2e_1012_bit0 -x_0x2e__0x2e__0x2e_1012_bit1 -x_0x2e__0x2e__0x2e_1012_bit2 -x_0x2e__0x2e__0x2e_1012_bit3 -x_0x2e__0x2e__0x2e_1013_bit0 -x_0x2e__0x2e__0x2e_1013_bit1 -x_0x2e__0x2e__0x2e_1013_bit2 -x_0x2e__0x2e__0x2e_1014_bit0 -x_0x2e__0x2e__0x2e_1014_bit1 -x_0x2e__0x2e__0x2e_1014_bit2 -x_0x2e__0x2e__0x2e_1015_bit0 -x_0x2e__0x2e__0x2e_1015_bit1 -x_0x2e__0x2e__0x2e_1016_bit0 -x_0x2e__0x2e__0x2e_1016_bit1 -x_0x2e__0x2e__0x2e_1017_bit0 x_0x2e__0x2e__0x2e_1110_bit0 -x_0x2e__0x2e__0x2e_1110_bit1 -x_0x2e__0x2e__0x2e_1110_bit2 -x_0x2e__0x2e__0x2e_1111_bit0 -x_0x2e__0x2e__0x2e_1111_bit1 -x_0x2e__0x2e__0x2e_1111_bit2 x_0x2e__0x2e__0x2e_1112_bit0 -x_0x2e__0x2e__0x2e_1112_bit1 -x_0x2e__0x2e__0x2e_1112_bit2 -x_0x2e__0x2e__0x2e_1112_bit3 x_0x2e__0x2e__0x2e_1113_bit0 -x_0x2e__0x2e__0x2e_1113_bit1 -x_0x2e__0x2e__0x2e_1113_bit2 -x_0x2e__0x2e__0x2e_1114_bit0 -x_0x2e__0x2e__0x2e_1114_bit1 -x_0x2e__0x2e__0x2e_1114_bit2 -x_0x2e__0x2e__0x2e_1115_bit0 -x_0x2e__0x2e__0x2e_1115_bit1 -x_0x2e__0x2e__0x2e_1116_bit0 -x_0x2e__0x2e__0x2e_1116_bit1 x_0x2e__0x2e__0x2e_1117_bit0 -x_0x2e__0x2e__0x2e_1210_bit0 -x_0x2e__0x2e__0x2e_1210_bit1 -x_0x2e__0x2e__0x2e_1210_bit2 -x_0x2e__0x2e__0x2e_1211_bit0 -x_0x2e__0x2e__0x2e_1211_bit1 -x_0x2e__0x2e__0x2e_1211_bit2 -x_0x2e__0x2e__0x2e_1212_bit0 -x_0x2e__0x2e__0x2e_1212_bit1 -x_0x2e__0x2e__0x2e_1212_bit2 -x_0x2e__0x2e__0x2e_1212_bit3 -x_0x2e__0x2e__0x2e_1213_bit0 -x_0x2e__0x2#### 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.91 0.97 0.99 2/54 6466 Raw data (stat): 6466 (runsolver) R 6465 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490832856 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99982 s] Raw data (loadavg): 0.93 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 8949 0 0 0 978 20 0 0 25 0 1 0 490832856 39116800 8315 4294967295 134512640 134672761 3221224624 3221223808 134558374 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9550 8315 603 41 0 9509 0 vsize: 38200 [startup+19.9996 s] Raw data (loadavg): 0.94 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9061 0 0 0 1977 21 0 0 25 0 1 0 490832856 39624704 8427 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9674 8427 603 41 0 9633 0 vsize: 38696 [startup+30.0001 s] Raw data (loadavg): 0.95 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9121 0 0 0 2977 21 0 0 25 0 1 0 490832856 39895040 8487 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9740 8487 603 41 0 9699 0 vsize: 38960 [startup+39.9993 s] Raw data (loadavg): 0.95 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9312 0 0 0 3977 21 0 0 25 0 1 0 490832856 40718336 8678 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9941 8678 603 41 0 9900 0 vsize: 39764 [startup+50.0003 s] Raw data (loadavg): 0.96 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9489 0 0 0 4976 22 0 0 25 0 1 0 490832856 41390080 8855 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10105 8855 603 41 0 10064 0 vsize: 40420 [startup+60.0011 s] Raw data (loadavg): 0.97 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9619 0 0 0 5976 22 0 0 25 0 1 0 490832856 41930752 8985 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10237 8985 603 41 0 10196 0 vsize: 40948 [startup+70.0011 s] Raw data (loadavg): 0.97 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9926 0 0 0 6975 23 0 0 25 0 1 0 490832856 43134976 9292 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10531 9292 603 41 0 10490 0 vsize: 42124 [startup+80.002 s] Raw data (loadavg): 0.98 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10130 0 0 0 7975 23 0 0 25 0 1 0 490832856 44036096 9496 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10751 9496 603 41 0 10710 0 vsize: 43004 [startup+90.0018 s] Raw data (loadavg): 0.98 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10282 0 0 0 8975 24 0 0 25 0 1 0 490832856 44695552 9648 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10912 9648 603 41 0 10871 0 vsize: 43648 [startup+100.002 s] Raw data (loadavg): 0.98 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10432 0 0 0 9975 24 0 0 25 0 1 0 490832856 45228032 9798 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11042 9798 603 41 0 11001 0 vsize: 44168 [startup+110.003 s] Raw data (loadavg): 0.98 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10563 0 0 0 10974 24 0 0 25 0 1 0 490832856 45760512 9929 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11172 9929 603 41 0 11131 0 vsize: 44688 [startup+120.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10855 0 0 0 11974 25 0 0 25 0 1 0 490832856 46968832 10221 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11467 10221 603 41 0 11426 0 vsize: 45868 [startup+130.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10921 0 0 0 12974 25 0 0 25 0 1 0 490832856 47239168 10287 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11533 10287 603 41 0 11492 0 vsize: 46132 [startup+140.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 11115 0 0 0 13973 26 0 0 25 0 1 0 490832856 48041984 10481 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11729 10481 603 41 0 11688 0 vsize: 46916 [startup+150.004 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 11411 0 0 0 14973 27 0 0 25 0 1 0 490832856 49385472 10777 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12057 10777 603 41 0 12016 0 vsize: 48228 [startup+160.005 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 11659 0 0 0 15972 28 0 0 25 0 1 0 490832856 50319360 11025 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12285 11025 603 41 0 12244 0 vsize: 49140 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 11944 0 0 0 16972 28 0 0 25 0 1 0 490832856 51548160 11310 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12585 11310 603 41 0 12544 0 vsize: 50340 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12178 0 0 0 17972 29 0 0 25 0 1 0 490832856 52461568 11544 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12808 11544 603 41 0 12767 0 vsize: 51232 [startup+190.005 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12350 0 0 0 18972 29 0 0 25 0 1 0 490832856 53256192 11716 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13002 11716 603 41 0 12961 0 vsize: 52008 [startup+200.005 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12449 0 0 0 19971 29 0 0 25 0 1 0 490832856 53653504 11815 4294967295 134512640 134672761 3221224624 3221223764 134560629 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13099 11815 603 41 0 13058 0 vsize: 52396 [startup+210.005 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12540 0 0 0 20971 30 0 0 25 0 1 0 490832856 53919744 11906 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13164 11906 603 41 0 13123 0 vsize: 52656 [startup+220.005 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12677 0 0 0 21971 30 0 0 25 0 1 0 490832856 54587392 12043 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13327 12043 603 41 0 13286 0 vsize: 53308 [startup+230.004 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12819 0 0 0 22971 30 0 0 25 0 1 0 490832856 55123968 12185 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13458 12185 603 41 0 13417 0 vsize: 53832 [startup+240.004 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12955 0 0 0 23970 31 0 0 25 0 1 0 490832856 55660544 12321 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13589 12321 603 41 0 13548 0 vsize: 54356 [startup+250.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 13126 0 0 0 24970 32 0 0 25 0 1 0 490832856 56352768 12492 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13758 12492 603 41 0 13717 0 vsize: 55032 [startup+260.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 13307 0 0 0 25970 32 0 0 25 0 1 0 490832856 57143296 12673 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13951 12673 603 41 0 13910 0 vsize: 55804 [startup+270.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19142 0 0 0 26958 44 0 0 25 0 1 0 490832856 83886080 17888 4294967295 134512640 134672761 3221224624 3221223772 1074754720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20480 17888 603 41 0 20439 0 vsize: 81920 [startup+280.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19239 0 0 0 27956 45 0 0 25 0 1 0 490832856 84021248 17985 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20513 17985 603 41 0 20472 0 vsize: 82052 [startup+290.004 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19391 0 0 0 28956 45 0 0 25 0 1 0 490832856 84692992 18137 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20677 18137 603 41 0 20636 0 vsize: 82708 [startup+300.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19526 0 0 0 29956 45 0 0 25 0 1 0 490832856 85241856 18272 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20811 18272 603 41 0 20770 0 vsize: 83244 [startup+310.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19590 0 0 0 30956 46 0 0 25 0 1 0 490832856 85504000 18336 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20875 18336 603 41 0 20834 0 vsize: 83500 [startup+320.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19653 0 0 0 31956 46 0 0 25 0 1 0 490832856 85639168 18399 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20908 18399 603 41 0 20867 0 vsize: 83632 [startup+330.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19965 0 0 0 32955 47 0 0 25 0 1 0 490832856 87248896 18711 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21301 18711 603 41 0 21260 0 vsize: 85204 [startup+340.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 20156 0 0 0 33955 47 0 0 25 0 1 0 490832856 88047616 18902 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21496 18902 603 41 0 21455 0 vsize: 85984 [startup+350.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 20169 0 0 0 34955 47 0 0 25 0 1 0 490832856 88047616 18915 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21496 18915 603 41 0 21455 0 vsize: 85984 [startup+360.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 20245 0 0 0 35955 47 0 0 25 0 1 0 490832856 88317952 18991 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21562 18991 603 41 0 21521 0 vsize: 86248 [startup+370.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 20264 0 0 0 36955 47 0 0 25 0 1 0 490832856 88453120 19010 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21595 19010 603 41 0 21554 0 vsize: 86380 [startup+380.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 25275 0 0 0 37944 59 0 0 25 0 1 0 490832856 103784448 23731 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25338 23731 603 41 0 25297 0 vsize: 101352 [startup+390.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 25313 0 0 0 38944 59 0 0 25 0 1 0 490832856 103927808 23769 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25373 23769 603 41 0 25332 0 vsize: 101492 [startup+400.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 25389 0 0 0 39944 59 0 0 25 0 1 0 490832856 104198144 23845 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25439 23845 603 41 0 25398 0 vsize: 101756 [startup+410.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 25426 0 0 0 40944 59 0 0 25 0 1 0 490832856 104333312 23882 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25472 23882 603 41 0 25431 0 vsize: 101888 [startup+420.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26105 0 0 0 41944 60 0 0 25 0 1 0 490832856 106266624 24271 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25944 24271 603 41 0 25903 0 vsize: 103776 [startup+430.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26106 0 0 0 42944 60 0 0 25 0 1 0 490832856 106266624 24272 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25944 24272 603 41 0 25903 0 vsize: 103776 [startup+440.002 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26109 0 0 0 43944 60 0 0 25 0 1 0 490832856 106266624 24275 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25944 24275 603 41 0 25903 0 vsize: 103776 [startup+450.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26155 0 0 0 44944 60 0 0 25 0 1 0 490832856 106409984 24321 4294967295 134512640 134672761 3221224624 3221223792 134561372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25979 24321 603 41 0 25938 0 vsize: 103916 [startup+460.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26246 0 0 0 45944 60 0 0 25 0 1 0 490832856 106807296 24412 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26076 24412 603 41 0 26035 0 vsize: 104304 [startup+470.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26305 0 0 0 46944 60 0 0 25 0 1 0 490832856 107065344 24471 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26139 24471 603 41 0 26098 0 vsize: 104556 [startup+480.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26358 0 0 0 47944 60 0 0 25 0 1 0 490832856 107200512 24524 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26172 24524 603 41 0 26131 0 vsize: 104688 [startup+490.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26412 0 0 0 48944 60 0 0 25 0 1 0 490832856 107474944 24578 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26239 24578 603 41 0 26198 0 vsize: 104956 [startup+500.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26452 0 0 0 49944 60 0 0 25 0 1 0 490832856 107610112 24618 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26272 24618 603 41 0 26231 0 vsize: 105088 [startup+510.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26467 0 0 0 50945 60 0 0 25 0 1 0 490832856 107745280 24633 4294967295 134512640 134672761 3221224624 3221223792 134561261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26305 24633 603 41 0 26264 0 vsize: 105220 [startup+520 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26626 0 0 0 51944 61 0 0 25 0 1 0 490832856 108273664 24792 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26434 24792 603 41 0 26393 0 vsize: 105736 [startup+530.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 27706 0 0 0 52941 64 0 0 25 0 1 0 490832856 114745344 25582 4294967295 134512640 134672761 3221224624 3221221656 134524843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28014 25582 603 41 0 27973 0 vsize: 112056 [startup+540.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 31714 0 0 0 53932 74 0 0 25 0 1 0 490832856 142872576 29590 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34881 29590 603 41 0 34840 0 vsize: 139524 [startup+550 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 31833 0 0 0 54932 74 0 0 25 0 1 0 490832856 143413248 29709 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35013 29709 603 41 0 34972 0 vsize: 140052 [startup+560 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 31898 0 0 0 55932 74 0 0 25 0 1 0 490832856 143679488 29774 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35078 29774 603 41 0 35037 0 vsize: 140312 [startup+570 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 31952 0 0 0 56932 75 0 0 25 0 1 0 490832856 143814656 29828 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35111 29828 603 41 0 35070 0 vsize: 140444 [startup+580 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32042 0 0 0 57932 75 0 0 25 0 1 0 490832856 144216064 29918 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35209 29918 603 41 0 35168 0 vsize: 140836 [startup+590 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32061 0 0 0 58932 75 0 0 25 0 1 0 490832856 144351232 29937 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35242 29937 603 41 0 35201 0 vsize: 140968 [startup+599.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32261 0 0 0 59931 75 0 0 25 0 1 0 490832856 145145856 30137 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35436 30137 603 41 0 35395 0 vsize: 141744 [startup+609.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32327 0 0 0 60931 75 0 0 25 0 1 0 490832856 145408000 30203 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35500 30203 603 41 0 35459 0 vsize: 142000 [startup+619.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32387 0 0 0 61931 76 0 0 25 0 1 0 490832856 145674240 30263 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35565 30263 603 41 0 35524 0 vsize: 142260 [startup+629.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32475 0 0 0 62931 76 0 0 25 0 1 0 490832856 145944576 30351 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35631 30351 603 41 0 35590 0 vsize: 142524 [startup+639.998 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32554 0 0 0 63931 76 0 0 25 0 1 0 490832856 146345984 30430 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35729 30430 603 41 0 35688 0 vsize: 142916 [startup+649.998 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32639 0 0 0 64931 76 0 0 25 0 1 0 490832856 146616320 30515 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35795 30515 603 41 0 35754 0 vsize: 143180 [startup+659.998 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32796 0 0 0 65931 77 0 0 25 0 1 0 490832856 147283968 30672 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35958 30672 603 41 0 35917 0 vsize: 143832 [startup+669.998 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33288 0 0 0 66930 77 0 0 25 0 1 0 490832856 149291008 31164 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36448 31164 603 41 0 36407 0 vsize: 145792 [startup+679.998 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33911 0 0 0 67929 79 0 0 25 0 1 0 490832856 150339584 31497 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36704 31497 603 41 0 36663 0 vsize: 146816 [startup+689.998 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33911 0 0 0 68929 79 0 0 25 0 1 0 490832856 150339584 31497 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36704 31497 603 41 0 36663 0 vsize: 146816 [startup+699.998 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33912 0 0 0 69930 79 0 0 25 0 1 0 490832856 150339584 31498 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36704 31498 603 41 0 36663 0 vsize: 146816 [startup+710 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33912 0 0 0 70930 79 0 0 25 0 1 0 490832856 150339584 31498 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36704 31498 603 41 0 36663 0 vsize: 146816 [startup+719.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33912 0 0 0 71930 79 0 0 25 0 1 0 490832856 150339584 31498 4294967295 134512640 134672761 3221224624 3221223840 134561999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36704 31498 603 41 0 36663 0 vsize: 146816 [startup+729.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33912 0 0 0 72930 79 0 0 25 0 1 0 490832856 150339584 31498 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36704 31498 603 41 0 36663 0 vsize: 146816 [startup+740.001 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33913 0 0 0 73930 79 0 0 25 0 1 0 490832856 150339584 31499 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36704 31499 603 41 0 36663 0 vsize: 146816 [startup+750 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33914 0 0 0 74931 79 0 0 25 0 1 0 490832856 150339584 31500 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36704 31500 603 41 0 36663 0 vsize: 146816 [startup+760 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33967 0 0 0 75931 79 0 0 25 0 1 0 490832856 150482944 31553 4294967295 134512640 134672761 3221224624 3221223808 134559583 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36739 31553 603 41 0 36698 0 vsize: 146956 [startup+770 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34015 0 0 0 76931 79 0 0 25 0 1 0 490832856 150781952 31601 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36812 31601 603 41 0 36771 0 vsize: 147248 [startup+780 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34059 0 0 0 77931 79 0 0 25 0 1 0 490832856 150917120 31645 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36845 31645 603 41 0 36804 0 vsize: 147380 [startup+790 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34446 0 0 0 78930 80 0 0 25 0 1 0 490832856 152510464 32032 4294967295 134512640 134672761 3221224624 3221223772 1074732988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37234 32032 603 41 0 37193 0 vsize: 148936 [startup+800 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34494 0 0 0 79930 81 0 0 25 0 1 0 490832856 152645632 32080 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37267 32080 603 41 0 37226 0 vsize: 149068 [startup+810 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34550 0 0 0 80930 81 0 0 25 0 1 0 490832856 152915968 32136 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37333 32136 603 41 0 37292 0 vsize: 149332 [startup+819.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34646 0 0 0 81929 81 0 0 25 0 1 0 490832856 153313280 32232 4294967295 134512640 134672761 3221224624 3221223760 134560694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37430 32232 603 41 0 37389 0 vsize: 149720 [startup+829.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34716 0 0 0 82929 81 0 0 25 0 1 0 490832856 153583616 32302 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37496 32302 603 41 0 37455 0 vsize: 149984 [startup+839.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34796 0 0 0 83929 82 0 0 25 0 1 0 490832856 153985024 32382 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37594 32382 603 41 0 37553 0 vsize: 150376 [startup+849.998 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34895 0 0 0 84929 82 0 0 25 0 1 0 490832856 154390528 32481 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37693 32481 603 41 0 37652 0 vsize: 150772 [startup+859.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34997 0 0 0 85929 82 0 0 25 0 1 0 490832856 154791936 32583 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37791 32583 603 41 0 37750 0 vsize: 151164 [startup+869.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35087 0 0 0 86929 82 0 0 25 0 1 0 490832856 155054080 32673 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37855 32673 603 41 0 37814 0 vsize: 151420 [startup+879.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35177 0 0 0 87929 83 0 0 25 0 1 0 490832856 155455488 32763 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37953 32763 603 41 0 37912 0 vsize: 151812 [startup+889.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35229 0 0 0 88929 83 0 0 25 0 1 0 490832856 155729920 32815 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38020 32815 603 41 0 37979 0 vsize: 152080 [startup+899.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35258 0 0 0 89929 83 0 0 25 0 1 0 490832856 155865088 32844 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38053 32844 603 41 0 38012 0 vsize: 152212 [startup+909.999 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35294 0 0 0 90929 83 0 0 25 0 1 0 490832856 156000256 32880 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38086 32880 603 41 0 38045 0 vsize: 152344 [startup+920.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35356 0 0 0 91929 84 0 0 25 0 1 0 490832856 156135424 32942 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38119 32942 603 41 0 38078 0 vsize: 152476 [startup+930.004 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35440 0 0 0 92929 84 0 0 25 0 1 0 490832856 156540928 33026 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38218 33026 603 41 0 38177 0 vsize: 152872 [startup+940.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35686 0 0 0 93929 85 0 0 25 0 1 0 490832856 157478912 33272 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38447 33272 603 41 0 38406 0 vsize: 153788 [startup+950.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35887 0 0 0 94928 85 0 0 25 0 1 0 490832856 158285824 33473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38644 33473 603 41 0 38603 0 vsize: 154576 [startup+960.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36096 0 0 0 95928 86 0 0 25 0 1 0 490832856 159215616 33682 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38871 33682 603 41 0 38830 0 vsize: 155484 [startup+970.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36124 0 0 0 96928 86 0 0 25 0 1 0 490832856 159354880 33710 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38905 33710 603 41 0 38864 0 vsize: 155620 [startup+980.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36214 0 0 0 97928 86 0 0 25 0 1 0 490832856 159752192 33800 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39002 33800 603 41 0 38961 0 vsize: 156008 [startup+990.003 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36330 0 0 0 98928 86 0 0 25 0 1 0 490832856 160157696 33916 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39101 33916 603 41 0 39060 0 vsize: 156404 [startup+1000 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36440 0 0 0 99928 86 0 0 25 0 1 0 490832856 160559104 34026 4294967295 134512640 134672761 3221224624 3221223796 134556685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39199 34026 603 41 0 39158 0 vsize: 156796 [startup+1010 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36441 0 0 0 100928 86 0 0 25 0 1 0 490832856 160559104 34027 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39199 34027 603 41 0 39158 0 vsize: 156796 [startup+1020 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36462 0 0 0 101928 86 0 0 25 0 1 0 490832856 160690176 34048 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39231 34048 603 41 0 39190 0 vsize: 156924 [startup+1030 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36493 0 0 0 102928 87 0 0 25 0 1 0 490832856 160821248 34079 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39263 34079 603 41 0 39222 0 vsize: 157052 [startup+1040 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36520 0 0 0 103928 87 0 0 25 0 1 0 490832856 160952320 34106 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39295 34106 603 41 0 39254 0 vsize: 157180 [startup+1050 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36570 0 0 0 104929 87 0 0 25 0 1 0 490832856 161087488 34156 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39328 34156 603 41 0 39287 0 vsize: 157312 [startup+1060 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37104 0 0 0 105927 88 0 0 25 0 1 0 490832856 161308672 34218 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39382 34218 603 41 0 39341 0 vsize: 157528 [startup+1070 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37107 0 0 0 106927 88 0 0 25 0 1 0 490832856 161443840 34221 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39415 34221 603 41 0 39374 0 vsize: 157660 [startup+1080 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37111 0 0 0 107927 88 0 0 25 0 1 0 490832856 161443840 34225 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39415 34225 603 41 0 39374 0 vsize: 157660 [startup+1090 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37139 0 0 0 108927 88 0 0 25 0 1 0 490832856 161443840 34253 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39415 34253 603 41 0 39374 0 vsize: 157660 [startup+1100 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37176 0 0 0 109927 88 0 0 25 0 1 0 490832856 162238464 34290 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39609 34290 603 41 0 39568 0 vsize: 158436 [startup+1110 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37234 0 0 0 110928 88 0 0 25 0 1 0 490832856 162373632 34348 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39642 34348 603 41 0 39601 0 vsize: 158568 [startup+1120 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37746 0 0 0 111926 90 0 0 25 0 1 0 490832856 162480128 34382 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39668 34382 603 41 0 39627 0 vsize: 158672 [startup+1130 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37746 0 0 0 112927 90 0 0 25 0 1 0 490832856 162480128 34382 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39668 34382 603 41 0 39627 0 vsize: 158672 [startup+1140 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37812 0 0 0 113927 90 0 0 25 0 1 0 490832856 162750464 34448 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39734 34448 603 41 0 39693 0 vsize: 158936 [startup+1150 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37898 0 0 0 114927 90 0 0 25 0 1 0 490832856 163160064 34534 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39834 34534 603 41 0 39793 0 vsize: 159336 [startup+1160 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37917 0 0 0 115927 90 0 0 25 0 1 0 490832856 163295232 34553 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39867 34553 603 41 0 39826 0 vsize: 159468 [startup+1170 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37928 0 0 0 116927 90 0 0 25 0 1 0 490832856 163295232 34564 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39867 34564 603 41 0 39826 0 vsize: 159468 [startup+1180 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37938 0 0 0 117927 90 0 0 25 0 1 0 490832856 163295232 34574 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39867 34574 603 41 0 39826 0 vsize: 159468 [startup+1190 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37948 0 0 0 118927 90 0 0 25 0 1 0 490832856 163295232 34584 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39867 34584 603 41 0 39826 0 vsize: 159468 [startup+1200 s] Raw data (loadavg): 0.99 0.97 0.99 2/54 6466 Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37977 0 0 0 119928 90 0 0 25 0 1 0 490832856 163430400 34613 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39900 34613 603 41 0 39859 0 vsize: 159600 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.99 1/54 6466 Raw data (stat): 6466 (minisat+) Z 6465 25347 25346 0 -1 12 37980 0 0 0 119928 97 0 0 25 0 1 0 490832856 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.07 CPU time (s): 1200.25 CPU user time (s): 1199.28 CPU system time (s): 0.971852 CPU usage (%): 100.015 Max. virtual memory (Kb): 159600 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####