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 wulflinc17 THE 2005-04-21 23:25:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13454 boxname=wulflinc17 idbench=1035 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f1382105ee9fb79777762a53cf6a73c1 /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-gt2.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-gt2.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-gt2.opb IDLAUNCH: 13454 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 868832 kB Buffers: 14732 kB Cached: 127028 kB SwapCached: 360 kB Active: 10132 kB Inactive: 134128 kB HighTotal: 131008 kB HighFree: 96684 kB LowTotal: 903652 kB LowFree: 772148 kB SwapTotal: 2097892 kB SwapFree: 2097056 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5860 kB Slab: 15856 kB Committed_AS: 63820 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 23:45:53 (client local time) WITH STATUS 10 IN 1200.21 SECONDS stats: 13454 7 1200.21 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]---> BDD-cost: 231 c ---[ 35]---> BDD-cost: 231 c ---[ 34]---> BDD-cost: 21 c ---[ 33]---> BDD-cost: 128 c ---[ 32]---> BDD-cost: 183 c ---[ 31]---> BDD-cost: 25 c ---[ 30]---> BDD-cost: 126 c ---[ 29]---> BDD-cost: 111 c ---[ 28]---> BDD-cost: 128 c ---[ 27]---> BDD-cost: 105 c ---[ 26]---> BDD-cost: 185 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]---> BDD-cost: 7378 c ---[ 9]---> BDD-cost: 669 c ---[ 8]---> BDD-cost: 76 c ---[ 7]---> BDD-cost: 1557 c ---[ 6]---> BDD-cost: 1215 c ---[ 5]---> BDD-cost: 48 c ---[ 4]---> BDD-cost: 114 c ---[ 3]---> BDD-cost: 55 c ---[ 2]---> BDD-cost: 2937 c ---[ 1]---> BDD-cost: 1052 c ---[ 0]---> BDD-cost: 92 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 45289 134500 | 15096 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 228152[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:92447 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 | 2 | 298890 726329 | 99630 2 12 6.0 | 0.000 % | c | 105 | 298124 724597 | 109593 101 535 5.3 | 0.281 % | c | 255 | 297317 722773 | 120552 250 5224 20.9 | 0.486 % | c | 480 | 295636 718946 | 132607 471 10583 22.5 | 0.945 % | c | 817 | 293957 715105 | 145868 806 24487 30.4 | 1.417 % | c | 1325 | 287505 700303 | 160455 1282 27144 21.2 | 3.285 % | c | 2086 | 274412 670155 | 176500 1959 41217 21.0 | 7.185 % | c ============================================================================== c [1mFound solution: 228107[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:72978 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 | 2182 | 455370 1091535 | 151790 2051 43708 21.3 | 7.185 % | c | 2282 | 455370 1091535 | 166969 2151 45808 21.3 | 7.218 % | c | 2432 | 450153 1079714 | 183665 2295 49252 21.5 | 8.191 % | c | 2657 | 450153 1079714 | 202032 2520 53000 21.0 | 8.191 % | c | 2994 | 441724 1060467 | 222235 2817 56525 20.1 | 9.728 % | c | 3500 | 441049 1058922 | 244459 3317 64078 19.3 | 9.849 % | c | 4259 | 441049 1058922 | 268905 4076 70538 17.3 | 9.849 % | c | 5398 | 441049 1058922 | 295795 5215 81194 15.6 | 9.849 % | c | 7108 | 440946 1058682 | 325375 6924 102009 14.7 | 9.869 % | c ============================================================================== c [1mFound solution: 228003[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:68318 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 | 7782 | 598189 1424680 | 199396 7400 107739 14.6 | 9.869 % | c | 7883 | 598038 1424335 | 219335 7499 109071 14.5 | 11.279 % | c | 8033 | 593293 1413534 | 241269 7260 106197 14.6 | 11.923 % | c | 8260 | 593279 1413501 | 265396 7440 120478 16.2 | 11.925 % | c ============================================================================== c [1mFound solution: 226571[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 | 8298 | 593064 1413790 | 197688 7476 124044 16.6 | 11.925 % | c | 8398 | 592851 1413314 | 217456 7572 125841 16.6 | 11.979 % | c | 8548 | 592248 1411977 | 239202 7719 126514 16.4 | 12.064 % | c ============================================================================== c [1mFound solution: 225156[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 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 | 8610 | 589147 1404947 | 196382 7720 126643 16.4 | 12.064 % | c | 8710 | 589147 1404947 | 216020 7820 127668 16.3 | 12.483 % | c | 8861 | 589147 1404947 | 237622 7971 128755 16.2 | 12.483 % | c | 9086 | 587881 1402070 | 261384 8192 130321 15.9 | 12.657 % | c | 9424 | 581084 1386553 | 287522 8444 131552 15.6 | 13.585 % | c | 9930 | 577887 1379236 | 316275 8856 141272 16.0 | 14.021 % | c | 10689 | 575421 1373584 | 347902 9496 146897 15.5 | 14.357 % | c | 11828 | 574402 1371278 | 382692 10609 187884 17.7 | 14.493 % | c | 13538 | 570586 1362558 | 420962 12281 264267 21.5 | 15.004 % | c | 16101 | 569103 1359156 | 463058 14831 402467 27.1 | 15.208 % | c | 19945 | 567496 1355462 | 509364 18667 828516 44.4 | 15.426 % | c ============================================================================== c [1mFound solution: 224882[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 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 | 20299 | 567509 1355605 | 189169 19021 836114 44.0 | 15.426 % | c | 20399 | 567509 1355605 | 208085 19121 840088 43.9 | 15.426 % | c | 20549 | 567329 1355202 | 228894 19269 844134 43.8 | 15.446 % | c | 20774 | 564229 1348123 | 251783 19421 844924 43.5 | 15.867 % | c | 21111 | 564229 1348123 | 276962 19758 850448 43.0 | 15.867 % | c | 21617 | 564126 1347891 | 304658 20263 857199 42.3 | 15.882 % | c | 22378 | 563650 1346812 | 335124 21011 862862 41.1 | 15.947 % | c | 23517 | 561569 1342052 | 368636 22103 881716 39.9 | 16.231 % | c ============================================================================== c [1mFound solution: 222653[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 | 24619 | 558563 1335130 | 186187 22960 956712 41.7 | 16.231 % | c | 24719 | 558563 1335130 | 204805 23060 958791 41.6 | 16.639 % | c | 24871 | 558539 1335075 | 225286 23211 963417 41.5 | 16.642 % | c | 25098 | 556797 1331061 | 247814 23357 966618 41.4 | 16.880 % | c | 25435 | 551457 1318704 | 272596 23537 966536 41.1 | 17.622 % | c | 25941 | 551302 1318351 | 299856 24037 977475 40.7 | 17.643 % | c | 26703 | 551302 1318351 | 329841 24799 1021116 41.2 | 17.643 % | c ============================================================================== c [1mFound solution: 120481[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 | 26816 | 551347 1318463 | 183782 24912 1024011 41.1 | 17.643 % | c | 26918 | 551301 1318356 | 202160 25013 1025225 41.0 | 17.649 % | c | 27068 | 551301 1318356 | 222376 25163 1031087 41.0 | 17.649 % | c | 27296 | 551301 1318356 | 244613 25391 1065796 42.0 | 17.649 % | c | 27633 | 549875 1315069 | 269075 25550 1084183 42.4 | 17.844 % | c | 28139 | 549517 1314253 | 295982 26053 1088933 41.8 | 17.889 % | c | 28899 | 548230 1311311 | 325581 26791 1097334 41.0 | 18.056 % | c | 30038 | 543493 1300399 | 358139 27750 1115651 40.2 | 18.701 % | c ============================================================================== c [1mFound solution: 119791[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 | 30534 | 543495 1300408 | 181165 28245 1134636 40.2 | 18.701 % | c | 30634 | 542867 1298964 | 199281 28327 1137163 40.1 | 18.787 % | c | 30787 | 542867 1298964 | 219209 28480 1140643 40.1 | 18.787 % | c | 31012 | 542867 1298964 | 241130 28705 1152607 40.2 | 18.787 % | c | 31349 | 538587 1289074 | 265243 28715 1156875 40.3 | 19.378 % | c | 31855 | 538397 1288634 | 291768 29217 1161472 39.8 | 19.404 % | c | 32614 | 537715 1287065 | 320944 29869 1170464 39.2 | 19.497 % | c | 33753 | 537468 1286494 | 353039 30995 1187597 38.3 | 19.532 % | c | 35462 | 533253 1276753 | 388343 32596 1263680 38.8 | 20.112 % | c ============================================================================== c [1mFound solution: 118096[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 | 35657 | 533267 1276787 | 177755 32791 1284635 39.2 | 20.112 % | c | 35757 | 533267 1276787 | 195530 32891 1287773 39.2 | 20.112 % | c | 35907 | 532417 1274825 | 215083 32963 1288290 39.1 | 20.229 % | c | 36132 | 532417 1274825 | 236591 33188 1299883 39.2 | 20.229 % | c | 36469 | 532417 1274825 | 260251 33525 1302922 38.9 | 20.229 % | c | 36975 | 531944 1273732 | 286276 33906 1320618 38.9 | 20.296 % | c | 37734 | 531944 1273732 | 314903 34665 1341440 38.7 | 20.296 % | c | 38874 | 531861 1273544 | 346394 35803 1419556 39.6 | 20.307 % | c | 40582 | 530900 1271335 | 381033 37504 1515069 40.4 | 20.437 % | c ============================================================================== c [1mFound solution: 116340[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 41153 | 530748 1270984 | 176916 38066 1536021 40.4 | 20.437 % | c | 41253 | 529765 1268705 | 194607 38156 1537843 40.3 | 20.596 % | c | 41404 | 527957 1264539 | 214068 38170 1538217 40.3 | 20.841 % | c | 41629 | 526967 1262274 | 235475 38379 1546527 40.3 | 20.973 % | c | 41967 | 526967 1262274 | 259022 38717 1552391 40.1 | 20.973 % | c | 42473 | 526311 1260774 | 284924 39078 1554205 39.8 | 21.060 % | c | 43233 | 526311 1260774 | 313417 39838 1564762 39.3 | 21.060 % | c | 44374 | 525407 1258697 | 344759 40934 1610696 39.3 | 21.184 % | c | 46082 | 524738 1257157 | 379235 42622 1729510 40.6 | 21.277 % | c ============================================================================== c [1mFound solution: 112950[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 | 46141 | 524322 1256197 | 174774 42680 1736911 40.7 | 21.277 % | c | 46241 | 524322 1256197 | 192251 42780 1740112 40.7 | 21.336 % | c | 46394 | 524322 1256197 | 211476 42933 1741348 40.6 | 21.336 % | c | 46620 | 524322 1256197 | 232624 43159 1743123 40.4 | 21.336 % | c | 46957 | 524322 1256197 | 255886 43496 1745234 40.1 | 21.336 % | c | 47463 | 524322 1256197 | 281475 44002 1749672 39.8 | 21.336 % | c | 48222 | 523760 1254895 | 309622 44748 1761216 39.4 | 21.416 % | c | 49365 | 523760 1254895 | 340585 45891 1789036 39.0 | 21.416 % | c | 51074 | 523451 1254182 | 374643 47542 1918282 40.3 | 21.460 % | c | 53637 | 523230 1253676 | 412107 50100 2089988 41.7 | 21.489 % | c | 57482 | 519536 1245170 | 453318 53663 2331890 43.5 | 21.985 % | c ============================================================================== c [1mFound solution: 110854[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 | 57516 | 519310 1244651 | 173103 53695 2336515 43.5 | 21.985 % | c | 57616 | 519310 1244651 | 190413 53795 2338342 43.5 | 22.016 % | c | 57766 | 519310 1244651 | 209454 53945 2342960 43.4 | 22.016 % | c | 57993 | 519310 1244651 | 230400 54172 2346033 43.3 | 22.016 % | c | 58330 | 518541 1242880 | 253440 54482 2350570 43.1 | 22.121 % | c | 58836 | 517156 1239688 | 278784 54936 2353957 42.8 | 22.311 % | c | 59595 | 516045 1237127 | 306662 55665 2377705 42.7 | 22.463 % | c | 60735 | 515589 1236076 | 337328 56771 2459751 43.3 | 22.526 % | c ============================================================================== c [1mFound solution: 76236[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 61651 | 515612 1236131 | 171870 57687 2565392 44.5 | 22.526 % | c | 61751 | 515374 1235581 | 189057 57781 2570479 44.5 | 22.557 % | c | 61902 | 515374 1235581 | 207962 57932 2584955 44.6 | 22.557 % | c | 62127 | 515374 1235581 | 228758 58157 2599969 44.7 | 22.557 % | c | 62464 | 514964 1234631 | 251634 58440 2615640 44.8 | 22.615 % | c | 62971 | 513351 1230928 | 276798 58582 2619291 44.7 | 22.835 % | c | 63731 | 513351 1230928 | 304478 59342 2647464 44.6 | 22.835 % | c | 64870 | 513351 1230928 | 334926 60481 2666471 44.1 | 22.835 % | c ============================================================================== c [1mFound solution: 75858[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 | 66316 | 511544 1226747 | 170514 61832 2879140 46.6 | 22.835 % | c | 66417 | 511305 1226189 | 187565 61914 2889868 46.7 | 23.122 % | c | 66567 | 510740 1224874 | 206321 62053 2891563 46.6 | 23.203 % | c | 66792 | 510726 1224842 | 226954 62276 2898742 46.5 | 23.205 % | c ============================================================================== c [1mFound solution: 75739[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 | 66892 | 510498 1224314 | 170166 62374 2904417 46.6 | 23.205 % | c | 66992 | 510498 1224314 | 187182 62474 2909023 46.6 | 23.240 % | c | 67142 | 510498 1224314 | 205900 62624 2912865 46.5 | 23.240 % | c | 67369 | 508841 1220497 | 226490 62692 2913240 46.5 | 23.466 % | c | 67706 | 508821 1220450 | 249140 63016 2927307 46.5 | 23.469 % | c | 68213 | 507776 1218035 | 274054 63512 2993275 47.1 | 23.610 % | c ============================================================================== c [1mFound solution: 74881[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 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 | 68289 | 507789 1218067 | 169263 63588 3002926 47.2 | 23.610 % | c | 68392 | 507789 1218067 | 186189 63691 3017355 47.4 | 23.610 % | c | 68542 | 507323 1216992 | 204808 63828 3022418 47.4 | 23.677 % | c | 68767 | 506850 1215908 | 225289 63984 3030816 47.4 | 23.739 % | c ============================================================================== c [1mFound solution: 71337[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 | 69043 | 506863 1215947 | 168954 64260 3055644 47.6 | 23.739 % | c | 69145 | 505567 1212960 | 185849 64309 3057894 47.6 | 23.915 % | c ============================================================================== c [1mFound solution: 71054[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 | 69209 | 505562 1212956 | 168520 64372 3059874 47.5 | 23.915 % | c ============================================================================== c [1mFound solution: 69614[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 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 | 69239 | 505572 1212982 | 168524 64402 3061029 47.5 | 23.915 % | c | 69339 | 505572 1212982 | 185376 64502 3066241 47.5 | 23.916 % | c | 69490 | 505572 1212982 | 203914 64653 3070609 47.5 | 23.916 % | c | 69715 | 505572 1212982 | 224305 64878 3077896 47.4 | 23.916 % | c | 70053 | 505202 1212131 | 246735 65195 3100673 47.6 | 23.963 % | c ============================================================================== c [1mFound solution: 68795[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 70179 | 505216 1212166 | 168405 65321 3114607 47.7 | 23.963 % | c | 70279 | 505216 1212166 | 185245 65421 3115979 47.6 | 23.962 % | c | 70429 | 505123 1211953 | 203770 65570 3118930 47.6 | 23.974 % | c | 70654 | 504188 1209790 | 224147 65759 3121473 47.5 | 24.104 % | c | 70991 | 504188 1209790 | 246561 66096 3138484 47.5 | 24.104 % | c ============================================================================== c [1mFound solution: 68554[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 | 71011 | 504200 1209821 | 168066 66116 3141878 47.5 | 24.104 % | c | 71111 | 503917 1209163 | 184872 66212 3164635 47.8 | 24.146 % | c | 71263 | 503917 1209163 | 203359 66364 3167458 47.7 | 24.146 % | c | 71488 | 503842 1208992 | 223695 66584 3171024 47.6 | 24.156 % | c | 71827 | 503415 1208009 | 246065 66702 3173054 47.6 | 24.215 % | c | 72333 | 503138 1207370 | 270671 67017 3179237 47.4 | 24.254 % | c | 73093 | 502444 1205777 | 297739 67381 3200953 47.5 | 24.347 % | c ============================================================================== c [1mFound solution: 64777[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 73150 | 501869 1204457 | 167289 67422 3205237 47.5 | 24.347 % | c | 73251 | 501809 1204320 | 184017 67522 3216871 47.6 | 24.433 % | c | 73402 | 499991 1200109 | 202419 66414 3131920 47.2 | 24.681 % | c | 73627 | 498522 1196710 | 222661 66154 3130036 47.3 | 24.886 % | c | 73965 | 498515 1196695 | 244927 66489 3135457 47.2 | 24.887 % | c | 74471 | 497408 1194129 | 269420 66921 3147606 47.0 | 25.043 % | c | 75232 | 497216 1193682 | 296362 67677 3167750 46.8 | 25.070 % | c | 76371 | 497216 1193682 | 325998 68816 3212914 46.7 | 25.070 % | c | 78079 | 497210 1193668 | 358598 70520 3372262 47.8 | 25.071 % | c ============================================================================== c [1mFound solution: 64343[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:52219 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 | 78296 | 595370 1421212 | 198456 70737 3420063 48.3 | 25.071 % | c ============================================================================== c [1mFound solution: 64308[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 78341 | 595405 1421588 | 198468 70782 3424089 48.4 | 25.071 % | c | 78441 | 594640 1419832 | 218314 70873 3426664 48.3 | 25.761 % | c | 78591 | 593992 1418326 | 240146 70954 3430454 48.3 | 25.836 % | c | 78817 | 593992 1418326 | 264160 71180 3442997 48.4 | 25.836 % | c | 79155 | 593920 1418160 | 290576 71517 3478608 48.6 | 25.844 % | c | 79661 | 593836 1417966 | 319634 72015 3515965 48.8 | 25.853 % | c | 80421 | 591282 1412194 | 351598 72537 3570749 49.2 | 26.139 % | c | 81561 | 590980 1411521 | 386757 73670 3649538 49.5 | 26.173 % | c | 83270 | 590798 1411120 | 425433 75378 4503969 59.8 | 26.194 % | c | 85834 | 586920 1402191 | 467977 77813 4694498 60.3 | 26.638 % | c | 89678 | 586213 1400603 | 514774 81607 5103308 62.5 | 26.720 % | c ============================================================================== c [1mFound solution: 52018[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:65838 Base: 2 2 2 2 3 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90997 | 719458 1709984 | 239819 82576 5331159 64.6 | 26.720 % | c | 91097 | 718738 1708328 | 263800 82666 5337543 64.6 | 26.453 % | c | 91249 | 718738 1708328 | 290180 82818 5381999 65.0 | 26.453 % | c | 91475 | 718738 1708328 | 319199 83044 5413728 65.2 | 26.453 % | c | 91812 | 718383 1707517 | 351118 83376 5435360 65.2 | 26.486 % | c | 92318 | 718383 1707517 | 386230 83882 5443883 64.9 | 26.486 % | c | 93077 | 718383 1707517 | 424853 84641 5494325 64.9 | 26.486 % | c | 94219 | 716739 1703848 | 467339 85767 5575556 65.0 | 26.637 % | c | 95929 | 716739 1703848 | 514073 87477 5774198 66.0 | 26.637 % | c | 98491 | 715748 1701587 | 565480 90000 5988895 66.5 | 26.732 % | c ============================================================================== c [1mFound solution: 51169[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 3 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 99097 | 715770 1702086 | 238590 90606 6150562 67.9 | 26.732 % | c | 99197 | 715770 1702086 | 262449 90706 6154126 67.8 | 26.731 % | c | 99348 | 715770 1702086 | 288693 90857 6193168 68.2 | 26.731 % | c | 99574 | 715770 1702086 | 317563 91083 6195320 68.0 | 26.731 % | c | 99911 | 715770 1702086 | 349319 91420 6198919 67.8 | 26.731 % | c | 100419 | 715539 1701548 | 384251 91921 6203500 67.5 | 26.754 % | c | 101178 | 715539 1701548 | 422676 92680 6210496 67.0 | 26.754 % | c | 102317 | 715525 1701516 | 464944 93818 6273714 66.9 | 26.755 % | c | 104025 | 715452 1701358 | 511438 95525 6414020 67.1 | 26.762 % | c ============================================================================== c [1mFound solution: 50473[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 3 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 104106 | 715467 1701508 | 238489 95606 6444430 67.4 | 26.762 % | c | 104206 | 715467 1701508 | 262337 95706 6456108 67.5 | 26.762 % | c | 104358 | 715122 1700718 | 288571 95843 6464966 67.5 | 26.795 % | c | 104584 | 715122 1700718 | 317428 96069 6476632 67.4 | 26.795 % | c | 104921 | 714551 1699432 | 349171 96318 6481465 67.3 | 26.847 % | c | 105428 | 714551 1699432 | 384088 96825 6497453 67.1 | 26.847 % | 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_0#### 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.95 0.90 2/55 7238 Raw data (stat): 7238 (runsolver) R 7237 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549034218 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+10.0004 s] Raw data (loadavg): 0.93 0.95 0.90 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 9073 0 0 0 969 24 0 0 25 0 1 0 549034218 40308736 8722 4294967295 134512640 134672761 3221224544 3221223680 134560598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9841 8722 603 41 0 9800 0 vsize: 39364 [startup+20.0005 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 14818 0 0 0 1954 39 0 0 25 0 1 0 549034218 67272704 14137 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16424 14137 603 41 0 16383 0 vsize: 65696 [startup+30.0011 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 14848 0 0 0 2954 40 0 0 25 0 1 0 549034218 67272704 14167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16424 14167 603 41 0 16383 0 vsize: 65696 [startup+40.0012 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 14901 0 0 0 3953 40 0 0 25 0 1 0 549034218 67538944 14220 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16489 14220 603 41 0 16448 0 vsize: 65956 [startup+50.0013 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19653 0 0 0 4941 52 0 0 25 0 1 0 549034218 83431424 18972 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20369 18972 603 41 0 20328 0 vsize: 81476 [startup+60.0008 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19785 0 0 0 5941 53 0 0 25 0 1 0 549034218 83558400 19104 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20400 19104 603 41 0 20359 0 vsize: 81600 [startup+70.002 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19796 0 0 0 6941 53 0 0 25 0 1 0 549034218 83607552 19115 4294967295 134512640 134672761 3221224544 3221223728 134558500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20412 19115 603 41 0 20371 0 vsize: 81648 [startup+80.0021 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19812 0 0 0 7940 54 0 0 25 0 1 0 549034218 83742720 19131 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20445 19131 603 41 0 20404 0 vsize: 81780 [startup+90.0018 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19830 0 0 0 8940 54 0 0 25 0 1 0 549034218 83742720 19149 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20445 19149 603 41 0 20404 0 vsize: 81780 [startup+100.002 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19845 0 0 0 9940 55 0 0 25 0 1 0 549034218 83873792 19164 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20477 19164 603 41 0 20436 0 vsize: 81908 [startup+110.002 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19879 0 0 0 10940 55 0 0 25 0 1 0 549034218 84045824 19198 4294967295 134512640 134672761 3221224544 3221223600 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20519 19198 603 41 0 20478 0 vsize: 82076 [startup+120.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19920 0 0 0 11940 55 0 0 25 0 1 0 549034218 84180992 19239 4294967295 134512640 134672761 3221224544 3221223680 134560637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20552 19239 603 41 0 20511 0 vsize: 82208 [startup+130.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20058 0 0 0 12940 55 0 0 25 0 1 0 549034218 84721664 19377 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20684 19377 603 41 0 20643 0 vsize: 82736 [startup+140.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20317 0 0 0 13939 56 0 0 25 0 1 0 549034218 85852160 19636 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20960 19636 603 41 0 20919 0 vsize: 83840 [startup+150.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20482 0 0 0 14939 56 0 0 25 0 1 0 549034218 86540288 19801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21128 19801 603 41 0 21087 0 vsize: 84512 [startup+160.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20548 0 0 0 15939 56 0 0 25 0 1 0 549034218 86794240 19867 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21190 19867 603 41 0 21149 0 vsize: 84760 [startup+170.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20548 0 0 0 16939 56 0 0 25 0 1 0 549034218 86794240 19867 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21190 19867 603 41 0 21149 0 vsize: 84760 [startup+180.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20558 0 0 0 17939 56 0 0 25 0 1 0 549034218 86929408 19877 4294967295 134512640 134672761 3221224544 3221223808 134562492 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21223 19877 603 41 0 21182 0 vsize: 84892 [startup+190.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7238 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20625 0 0 0 18939 57 0 0 25 0 1 0 549034218 87199744 19944 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21289 19944 603 41 0 21248 0 vsize: 85156 [startup+200.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20674 0 0 0 19939 57 0 0 25 0 1 0 549034218 87293952 19993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21312 19993 603 41 0 21271 0 vsize: 85248 [startup+210.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20675 0 0 0 20939 57 0 0 25 0 1 0 549034218 87293952 19994 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21312 19994 603 41 0 21271 0 vsize: 85248 [startup+220.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20713 0 0 0 21939 57 0 0 25 0 1 0 549034218 87564288 20032 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21378 20032 603 41 0 21337 0 vsize: 85512 [startup+230.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20749 0 0 0 22939 57 0 0 25 0 1 0 549034218 87699456 20068 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21411 20068 603 41 0 21370 0 vsize: 85644 [startup+240.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20783 0 0 0 23939 57 0 0 25 0 1 0 549034218 87834624 20102 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21444 20102 603 41 0 21403 0 vsize: 85776 [startup+250 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20795 0 0 0 24939 58 0 0 25 0 1 0 549034218 87834624 20114 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21444 20114 603 41 0 21403 0 vsize: 85776 [startup+260 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20815 0 0 0 25939 58 0 0 25 0 1 0 549034218 87969792 20134 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21477 20134 603 41 0 21436 0 vsize: 85908 [startup+269.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20856 0 0 0 26939 58 0 0 25 0 1 0 549034218 88018944 20175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21489 20175 603 41 0 21448 0 vsize: 85956 [startup+280 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20856 0 0 0 27939 58 0 0 25 0 1 0 549034218 88018944 20175 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21489 20175 603 41 0 21448 0 vsize: 85956 [startup+290 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20878 0 0 0 28939 58 0 0 25 0 1 0 549034218 88150016 20197 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21521 20197 603 41 0 21480 0 vsize: 86084 [startup+299.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20963 0 0 0 29939 59 0 0 25 0 1 0 549034218 88551424 20282 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21619 20282 603 41 0 21578 0 vsize: 86476 [startup+309.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21009 0 0 0 30939 59 0 0 25 0 1 0 549034218 88813568 20328 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21683 20328 603 41 0 21642 0 vsize: 86732 [startup+319.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21030 0 0 0 31939 59 0 0 25 0 1 0 549034218 88948736 20349 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21716 20349 603 41 0 21675 0 vsize: 86864 [startup+330 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21092 0 0 0 32939 60 0 0 25 0 1 0 549034218 89083904 20411 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21749 20411 603 41 0 21708 0 vsize: 86996 [startup+340 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21186 0 0 0 33938 60 0 0 25 0 1 0 549034218 89485312 20505 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21847 20505 603 41 0 21806 0 vsize: 87388 [startup+350 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21248 0 0 0 34938 60 0 0 25 0 1 0 549034218 89751552 20567 4294967295 134512640 134672761 3221224544 3221223104 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21912 20567 603 41 0 21871 0 vsize: 87648 [startup+360 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21270 0 0 0 35938 61 0 0 25 0 1 0 549034218 89808896 20589 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21926 20589 603 41 0 21885 0 vsize: 87704 [startup+370 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21273 0 0 0 36938 61 0 0 25 0 1 0 549034218 89808896 20592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21926 20592 603 41 0 21885 0 vsize: 87704 [startup+380 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21422 0 0 0 37938 61 0 0 25 0 1 0 549034218 90476544 20741 4294967295 134512640 134672761 3221224544 3221223648 134559818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22089 20741 603 41 0 22048 0 vsize: 88356 [startup+390 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21493 0 0 0 38938 62 0 0 25 0 1 0 549034218 90701824 20812 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22144 20812 603 41 0 22103 0 vsize: 88576 [startup+400 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21550 0 0 0 39938 62 0 0 25 0 1 0 549034218 90968064 20869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22209 20869 603 41 0 22168 0 vsize: 88836 [startup+410 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21684 0 0 0 40938 62 0 0 25 0 1 0 549034218 91504640 21003 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22340 21003 603 41 0 22299 0 vsize: 89360 [startup+420.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21818 0 0 0 41937 63 0 0 25 0 1 0 549034218 92041216 21137 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22471 21137 603 41 0 22430 0 vsize: 89884 [startup+430 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21858 0 0 0 42937 63 0 0 25 0 1 0 549034218 92176384 21177 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22504 21177 603 41 0 22463 0 vsize: 90016 [startup+440 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22009 0 0 0 43937 63 0 0 25 0 1 0 549034218 92844032 21328 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22667 21328 603 41 0 22626 0 vsize: 90668 [startup+450.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22140 0 0 0 44936 64 0 0 25 0 1 0 549034218 93384704 21459 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22799 21459 603 41 0 22758 0 vsize: 91196 [startup+460 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22163 0 0 0 45937 64 0 0 25 0 1 0 549034218 93409280 21482 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22805 21482 603 41 0 22764 0 vsize: 91220 [startup+470 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22164 0 0 0 46937 64 0 0 25 0 1 0 549034218 93409280 21483 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22805 21483 603 41 0 22764 0 vsize: 91220 [startup+479.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22199 0 0 0 47937 64 0 0 25 0 1 0 549034218 93540352 21518 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22837 21518 603 41 0 22796 0 vsize: 91348 [startup+489.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7240 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22272 0 0 0 48937 64 0 0 25 0 1 0 549034218 93954048 21591 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22938 21591 603 41 0 22897 0 vsize: 91752 [startup+499.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22353 0 0 0 49937 64 0 0 25 0 1 0 549034218 94224384 21672 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23004 21672 603 41 0 22963 0 vsize: 92016 [startup+509.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22403 0 0 0 50937 65 0 0 25 0 1 0 549034218 94371840 21722 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23040 21722 603 41 0 22999 0 vsize: 92160 [startup+519.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22418 0 0 0 51937 65 0 0 25 0 1 0 549034218 94507008 21737 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23073 21737 603 41 0 23032 0 vsize: 92292 [startup+529.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22446 0 0 0 52937 65 0 0 25 0 1 0 549034218 94638080 21765 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23105 21765 603 41 0 23064 0 vsize: 92420 [startup+539.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22458 0 0 0 53937 65 0 0 25 0 1 0 549034218 94638080 21777 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23105 21777 603 41 0 23064 0 vsize: 92420 [startup+549.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22487 0 0 0 54937 65 0 0 25 0 1 0 549034218 94769152 21806 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23137 21806 603 41 0 23096 0 vsize: 92548 [startup+559.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22520 0 0 0 55937 65 0 0 25 0 1 0 549034218 94904320 21839 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23170 21839 603 41 0 23129 0 vsize: 92680 [startup+569.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22743 0 0 0 56937 65 0 0 25 0 1 0 549034218 95752192 22062 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23377 22062 603 41 0 23336 0 vsize: 93508 [startup+579.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22779 0 0 0 57937 65 0 0 25 0 1 0 549034218 95887360 22098 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23410 22098 603 41 0 23369 0 vsize: 93640 [startup+589.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22780 0 0 0 58937 66 0 0 25 0 1 0 549034218 95887360 22099 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23410 22099 603 41 0 23369 0 vsize: 93640 [startup+599.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22807 0 0 0 59937 66 0 0 25 0 1 0 549034218 96022528 22126 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23443 22126 603 41 0 23402 0 vsize: 93772 [startup+609.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22851 0 0 0 60937 66 0 0 25 0 1 0 549034218 96292864 22170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23509 22170 603 41 0 23468 0 vsize: 94036 [startup+619.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22886 0 0 0 61937 66 0 0 25 0 1 0 549034218 96321536 22205 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23516 22205 603 41 0 23475 0 vsize: 94064 [startup+629.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22921 0 0 0 62937 66 0 0 25 0 1 0 549034218 96456704 22240 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23549 22240 603 41 0 23508 0 vsize: 94196 [startup+639.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22948 0 0 0 63937 67 0 0 25 0 1 0 549034218 96575488 22267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23578 22267 603 41 0 23537 0 vsize: 94312 [startup+649.997 s] Raw data (loadavg): 1.07 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22950 0 0 0 64937 67 0 0 25 0 1 0 549034218 96575488 22269 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23578 22269 603 41 0 23537 0 vsize: 94312 [startup+659.997 s] Raw data (loadavg): 1.06 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23011 0 0 0 65936 67 0 0 25 0 1 0 549034218 97091584 22330 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23704 22330 603 41 0 23663 0 vsize: 94816 [startup+669.998 s] Raw data (loadavg): 1.05 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23016 0 0 0 66936 67 0 0 25 0 1 0 549034218 97091584 22335 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23704 22335 603 41 0 23663 0 vsize: 94816 [startup+679.997 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23048 0 0 0 67936 67 0 0 25 0 1 0 549034218 97345536 22367 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23766 22367 603 41 0 23725 0 vsize: 95064 [startup+689.997 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23055 0 0 0 68937 68 0 0 25 0 1 0 549034218 97345536 22374 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23766 22374 603 41 0 23725 0 vsize: 95064 [startup+699.997 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23057 0 0 0 69937 68 0 0 25 0 1 0 549034218 97345536 22376 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23766 22376 603 41 0 23725 0 vsize: 95064 [startup+709.997 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23090 0 0 0 70936 68 0 0 25 0 1 0 549034218 97476608 22409 4294967295 134512640 134672761 3221224544 3221223728 134557999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23798 22409 603 41 0 23757 0 vsize: 95192 [startup+719.998 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23119 0 0 0 71937 68 0 0 25 0 1 0 549034218 97521664 22438 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23809 22438 603 41 0 23768 0 vsize: 95236 [startup+729.997 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23119 0 0 0 72937 68 0 0 25 0 1 0 549034218 97521664 22438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23809 22438 603 41 0 23768 0 vsize: 95236 [startup+739.997 s] Raw data (loadavg): 1.09 1.00 0.92 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23119 0 0 0 73937 68 0 0 25 0 1 0 549034218 97521664 22438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23809 22438 603 41 0 23768 0 vsize: 95236 [startup+749.997 s] Raw data (loadavg): 1.07 1.00 0.92 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23120 0 0 0 74937 68 0 0 25 0 1 0 549034218 97521664 22439 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23809 22439 603 41 0 23768 0 vsize: 95236 [startup+759.997 s] Raw data (loadavg): 1.06 1.00 0.92 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23121 0 0 0 75937 68 0 0 25 0 1 0 549034218 97521664 22440 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23809 22440 603 41 0 23768 0 vsize: 95236 [startup+769.997 s] Raw data (loadavg): 1.05 1.00 0.92 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23330 0 0 0 76937 69 0 0 25 0 1 0 549034218 98467840 22649 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24040 22649 603 41 0 23999 0 vsize: 96160 [startup+779.997 s] Raw data (loadavg): 1.04 1.00 0.92 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26600 0 0 0 77928 77 0 0 25 0 1 0 549034218 129404928 25919 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31593 25919 603 41 0 31552 0 vsize: 126372 [startup+789.996 s] Raw data (loadavg): 1.04 1.00 0.92 2/55 7242 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26612 0 0 0 78928 77 0 0 25 0 1 0 549034218 129540096 25931 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31626 25931 603 41 0 31585 0 vsize: 126504 [startup+799.995 s] Raw data (loadavg): 1.03 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26673 0 0 0 79928 78 0 0 25 0 1 0 549034218 129675264 25992 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31659 25992 603 41 0 31618 0 vsize: 126636 [startup+809.996 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26694 0 0 0 80928 78 0 0 25 0 1 0 549034218 129814528 26013 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31693 26013 603 41 0 31652 0 vsize: 126772 [startup+819.996 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26769 0 0 0 81928 78 0 0 25 0 1 0 549034218 130084864 26088 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31759 26088 603 41 0 31718 0 vsize: 127036 [startup+829.995 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26835 0 0 0 82928 78 0 0 25 0 1 0 549034218 130355200 26154 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31825 26154 603 41 0 31784 0 vsize: 127300 [startup+839.995 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26902 0 0 0 83928 78 0 0 25 0 1 0 549034218 130625536 26221 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31891 26221 603 41 0 31850 0 vsize: 127564 [startup+849.995 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27024 0 0 0 84928 79 0 0 25 0 1 0 549034218 131133440 26343 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32015 26343 603 41 0 31974 0 vsize: 128060 [startup+859.995 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27124 0 0 0 85928 79 0 0 25 0 1 0 549034218 131522560 26443 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32110 26443 603 41 0 32069 0 vsize: 128440 [startup+869.995 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27324 0 0 0 86928 80 0 0 25 0 1 0 549034218 132501504 26643 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32349 26643 603 41 0 32308 0 vsize: 129396 [startup+879.995 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27505 0 0 0 87927 80 0 0 25 0 1 0 549034218 133263360 26824 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32535 26824 603 41 0 32494 0 vsize: 130140 [startup+889.995 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27650 0 0 0 88927 81 0 0 25 0 1 0 549034218 133885952 26969 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32687 26969 603 41 0 32646 0 vsize: 130748 [startup+899.996 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27690 0 0 0 89927 81 0 0 25 0 1 0 549034218 134021120 27009 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32720 27009 603 41 0 32679 0 vsize: 130880 [startup+909.995 s] Raw data (loadavg): 1.00 1.00 0.92 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27771 0 0 0 90927 81 0 0 25 0 1 0 549034218 134291456 27090 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32786 27090 603 41 0 32745 0 vsize: 131144 [startup+919.995 s] Raw data (loadavg): 1.08 1.02 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27912 0 0 0 91926 82 0 0 25 0 1 0 549034218 134963200 27231 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32950 27231 603 41 0 32909 0 vsize: 131800 [startup+929.995 s] Raw data (loadavg): 1.06 1.02 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 28054 0 0 0 92926 82 0 0 25 0 1 0 549034218 135499776 27373 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33081 27373 603 41 0 33040 0 vsize: 132324 [startup+939.994 s] Raw data (loadavg): 1.05 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 28354 0 0 0 93925 83 0 0 25 0 1 0 549034218 136695808 27673 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33373 27673 603 41 0 33332 0 vsize: 133492 [startup+949.995 s] Raw data (loadavg): 1.04 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 28380 0 0 0 94925 83 0 0 25 0 1 0 549034218 136822784 27699 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33404 27699 603 41 0 33363 0 vsize: 133616 [startup+959.994 s] Raw data (loadavg): 1.04 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 28466 0 0 0 95925 84 0 0 25 0 1 0 549034218 137093120 27785 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33470 27785 603 41 0 33429 0 vsize: 133880 [startup+969.995 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34225 0 0 0 96913 96 0 0 25 0 1 0 549034218 153686016 32885 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37521 32885 603 41 0 37480 0 vsize: 150084 [startup+979.994 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34312 0 0 0 97913 96 0 0 25 0 1 0 549034218 153821184 32972 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37554 32972 603 41 0 37513 0 vsize: 150216 [startup+989.994 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34359 0 0 0 98913 97 0 0 25 0 1 0 549034218 154087424 33019 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37619 33019 603 41 0 37578 0 vsize: 150476 [startup+999.995 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34378 0 0 0 99913 97 0 0 25 0 1 0 549034218 154087424 33038 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37619 33038 603 41 0 37578 0 vsize: 150476 [startup+1009.99 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34444 0 0 0 100913 97 0 0 25 0 1 0 549034218 154353664 33104 4294967295 134512640 134672761 3221224544 3221223680 134560613 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37684 33104 603 41 0 37643 0 vsize: 150736 [startup+1019.99 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34545 0 0 0 101912 98 0 0 25 0 1 0 549034218 154750976 33205 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37781 33205 603 41 0 37740 0 vsize: 151124 [startup+1029.99 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34582 0 0 0 102912 98 0 0 25 0 1 0 549034218 154882048 33242 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37813 33242 603 41 0 37772 0 vsize: 151252 [startup+1039.99 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34629 0 0 0 103912 98 0 0 25 0 1 0 549034218 155152384 33289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37879 33289 603 41 0 37838 0 vsize: 151516 [startup+1049.99 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34666 0 0 0 104912 98 0 0 25 0 1 0 549034218 155291648 33326 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37913 33326 603 41 0 37872 0 vsize: 151652 [startup+1059.99 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34694 0 0 0 105912 98 0 0 25 0 1 0 549034218 155426816 33354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37946 33355 603 41 0 37905 0 vsize: 151784 [startup+1069.99 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34749 0 0 0 106912 99 0 0 25 0 1 0 549034218 155561984 33409 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37979 33409 603 41 0 37938 0 vsize: 151916 [startup+1079.99 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34973 0 0 0 107911 100 0 0 25 0 1 0 549034218 156491776 33633 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38206 33633 603 41 0 38165 0 vsize: 152824 [startup+1090 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7244 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35136 0 0 0 108911 100 0 0 25 0 1 0 549034218 157155328 33796 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38368 33796 603 41 0 38327 0 vsize: 153472 [startup+1100 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35247 0 0 0 109911 101 0 0 25 0 1 0 549034218 157278208 33907 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38398 33907 603 41 0 38357 0 vsize: 153592 [startup+1110 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35280 0 0 0 110911 101 0 0 25 0 1 0 549034218 157417472 33940 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38432 33940 603 41 0 38391 0 vsize: 153728 [startup+1120 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35297 0 0 0 111911 101 0 0 25 0 1 0 549034218 157552640 33957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38465 33957 603 41 0 38424 0 vsize: 153860 [startup+1130 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35312 0 0 0 112911 101 0 0 25 0 1 0 549034218 157552640 33972 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38465 33972 603 41 0 38424 0 vsize: 153860 [startup+1140 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35345 0 0 0 113911 101 0 0 25 0 1 0 549034218 157687808 34005 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38498 34005 603 41 0 38457 0 vsize: 153992 [startup+1150 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35419 0 0 0 114911 101 0 0 25 0 1 0 549034218 158085120 34079 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38595 34079 603 41 0 38554 0 vsize: 154380 [startup+1160 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35569 0 0 0 115911 102 0 0 25 0 1 0 549034218 158597120 34229 4294967295 134512640 134672761 3221224544 3221223844 134556680 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38720 34229 603 41 0 38679 0 vsize: 154880 [startup+1170 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35569 0 0 0 116911 102 0 0 25 0 1 0 549034218 158597120 34229 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38720 34229 603 41 0 38679 0 vsize: 154880 [startup+1180 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35581 0 0 0 117911 102 0 0 25 0 1 0 549034218 158728192 34241 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38752 34241 603 41 0 38711 0 vsize: 155008 [startup+1190 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35588 0 0 0 118911 102 0 0 25 0 1 0 549034218 158728192 34248 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38752 34248 603 41 0 38711 0 vsize: 155008 [startup+1200 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 7246 Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35600 0 0 0 119911 102 0 0 25 0 1 0 549034218 158728192 34260 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38752 34260 603 41 0 38711 0 vsize: 155008 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 1.00 1.00 0.93 1/55 7246 Raw data (stat): 7238 (minisat+) Z 7237 20838 20837 0 -1 12 35603 0 0 0 119911 109 0 0 25 0 1 0 549034218 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.21 CPU user time (s): 1199.12 CPU system time (s): 1.09383 CPU usage (%): 100.012 Max. virtual memory (Kb): 155008 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####