Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-misc07.opb |
MD5SUM | 54df16ee65da54d5975ffedee80d2bb9 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1408128 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 21 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 2097151 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 1048576 |
Number of bits of the biggest number in a constraint | 21 |
Biggest sum of numbers in a constraint | 11486079 |
Number of bits of the biggest sum of numbers | 24 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 280 |
Total number of constraints | 471 |
Number of constraints which are clauses | 127 |
Number of constraints which are cardinality constraints (but not clauses) | 272 |
Number of constraints which are nor clauses,nor cardinality constraints | 72 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 253 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc1 THE 2005-04-21 02:56:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18590 boxname=wulflinc1 idbench=1430 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 54df16ee65da54d5975ffedee80d2bb9 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-misc07.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-misc07.opb IDLAUNCH: 18590 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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 : 2 cpu MHz : 451.053 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: 600740 kB Buffers: 23216 kB Cached: 383084 kB SwapCached: 0 kB Active: 110328 kB Inactive: 299108 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 600488 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7220 kB Slab: 18796 kB Committed_AS: 92820 kB PageTables: 344 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 03:16:11 (client local time) WITH STATUS 10 IN 1200.19 SECONDS stats: 18590 7 1200.19 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 247 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################### c -- Clauses(.)/Splits(s): ............................................................................................................................... c ---[ 245]---> Adder-cost: 1695 maxlim: 1048703 bits: 22/21 c ---[ 243]---> BDD-cost: 51 c ---[ 241]---> BDD-cost: 51 c ---[ 239]---> BDD-cost: 51 c ---[ 237]---> BDD-cost: 51 c ---[ 235]---> BDD-cost: 51 c ---[ 233]---> BDD-cost: 51 c ---[ 231]---> BDD-cost: 51 c ---[ 230]---> BDD-cost: 239 c ---[ 229]---> BDD-cost: 239 c ---[ 228]---> BDD-cost: 239 c ---[ 99]---> Sorter-cost: 127 Base: c ---[ 97]---> Sorter-cost: 127 Base: c ---[ 95]---> Sorter-cost: 127 Base: c ---[ 93]---> Sorter-cost: 127 Base: c ---[ 91]---> Sorter-cost: 127 Base: c ---[ 89]---> Sorter-cost: 127 Base: c ---[ 87]---> Sorter-cost: 127 Base: c ---[ 85]---> Sorter-cost: 127 Base: c ---[ 83]---> Sorter-cost: 127 Base: c ---[ 81]---> Sorter-cost: 127 Base: c ---[ 79]---> Sorter-cost: 127 Base: c ---[ 77]---> Sorter-cost: 127 Base: c ---[ 75]---> Sorter-cost: 127 Base: c ---[ 73]---> Sorter-cost: 127 Base: c ---[ 71]---> Sorter-cost: 127 Base: c ---[ 69]---> Sorter-cost: 127 Base: c ---[ 67]---> Sorter-cost: 127 Base: c ---[ 65]---> Sorter-cost: 127 Base: c ---[ 63]---> Sorter-cost: 127 Base: c ---[ 61]---> Sorter-cost: 127 Base: c ---[ 59]---> Sorter-cost: 127 Base: c ---[ 57]---> Sorter-cost: 127 Base: c ---[ 55]---> Sorter-cost: 127 Base: c ---[ 53]---> Sorter-cost: 127 Base: c ---[ 51]---> Sorter-cost: 127 Base: c ---[ 49]---> Sorter-cost: 127 Base: c ---[ 47]---> Sorter-cost: 127 Base: c ---[ 46]---> BDD-cost: 23 c ---[ 45]---> BDD-cost: 23 c ---[ 44]---> BDD-cost: 23 c ---[ 43]---> BDD-cost: 7 c ---[ 42]---> BDD-cost: 7 c ---[ 41]---> BDD-cost: 27 c ---[ 40]---> BDD-cost: 27 c ---[ 39]---> BDD-cost: 27 c ---[ 38]---> BDD-cost: 27 c ---[ 37]---> BDD-cost: 27 c ---[ 36]---> BDD-cost: 27 c ---[ 35]---> BDD-cost: 50 c ---[ 34]---> BDD-cost: 50 c ---[ 33]---> BDD-cost: 50 c ---[ 32]---> BDD-cost: 27 c ---[ 31]---> BDD-cost: 27 c ---[ 30]---> BDD-cost: 27 c ---[ 29]---> BDD-cost: 48 c ---[ 28]---> BDD-cost: 48 c ---[ 27]---> BDD-cost: 48 c ---[ 26]---> BDD-cost: 27 c ---[ 25]---> BDD-cost: 27 c ---[ 24]---> BDD-cost: 27 c ---[ 23]---> BDD-cost: 50 c ---[ 22]---> BDD-cost: 50 c ---[ 21]---> BDD-cost: 50 c ---[ 20]---> BDD-cost: 27 c ---[ 19]---> BDD-cost: 27 c ---[ 18]---> BDD-cost: 27 c ---[ 17]---> BDD-cost: 48 c ---[ 16]---> BDD-cost: 48 c ---[ 15]---> BDD-cost: 48 c ---[ 14]---> BDD-cost: 27 c ---[ 13]---> BDD-cost: 27 c ---[ 12]---> BDD-cost: 27 c ---[ 11]---> BDD-cost: 50 c ---[ 10]---> BDD-cost: 50 c ---[ 9]---> BDD-cost: 50 c ---[ 8]---> BDD-cost: 27 c ---[ 7]---> BDD-cost: 27 c ---[ 6]---> BDD-cost: 27 c ---[ 5]---> BDD-cost: 48 c ---[ 4]---> BDD-cost: 48 c ---[ 3]---> BDD-cost: 48 c ---[ 2]---> BDD-cost: 27 c ---[ 1]---> BDD-cost: 27 c ---[ 0]---> BDD-cost: 27 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 31883 102562 | 10627 0 0 nan | 0.000 % | c | 101 | 31878 102547 | 11689 94 1234 13.1 | 2.691 % | c ============================================================================== c [1mFound solution: 1584768[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 147 | 31900 102604 | 10633 140 2787 19.9 | 2.691 % | c | 247 | 31900 102604 | 11696 240 5379 22.4 | 2.703 % | c | 397 | 31886 102568 | 12865 389 8513 21.9 | 2.746 % | c ============================================================================== c [1mFound solution: 1549568[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 449 | 31901 102608 | 10633 440 9803 22.3 | 2.746 % | c | 550 | 31901 102608 | 11696 541 14876 27.5 | 2.801 % | c | 702 | 31901 102608 | 12865 693 25057 36.2 | 2.801 % | c ============================================================================== c [1mFound solution: 1548928[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 785 | 31897 102606 | 10632 774 25868 33.4 | 2.801 % | c | 885 | 31897 102606 | 11695 874 39547 45.2 | 2.928 % | c | 1035 | 31879 102561 | 12864 1020 40842 40.0 | 2.986 % | c | 1262 | 31838 102470 | 14151 1242 64042 51.6 | 3.159 % | c | 1599 | 31713 102156 | 15566 1562 76214 48.8 | 3.621 % | c | 2106 | 31713 102156 | 17122 2069 137467 66.4 | 3.620 % | c | 2866 | 31713 102156 | 18835 2829 192760 68.1 | 3.620 % | c ============================================================================== c [1mFound solution: 1539968[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3731 | 31734 102211 | 10578 3694 264070 71.5 | 3.620 % | c | 3832 | 31734 102211 | 11635 3795 265017 69.8 | 3.632 % | c | 3982 | 31734 102211 | 12799 3945 269841 68.4 | 3.632 % | c | 4208 | 31723 102187 | 14079 4169 287123 68.9 | 3.675 % | c | 4547 | 31667 102062 | 15487 4483 316090 70.5 | 3.920 % | c | 5055 | 31643 101978 | 17035 4985 326816 65.6 | 3.949 % | c ============================================================================== c [1mFound solution: 1534208[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5130 | 31668 102039 | 10556 5060 332463 65.7 | 3.949 % | c | 5230 | 31668 102039 | 11611 5160 334136 64.8 | 3.959 % | c | 5382 | 31668 102039 | 12772 5312 349661 65.8 | 3.959 % | c | 5607 | 31663 102024 | 14050 5534 369608 66.8 | 3.974 % | c ============================================================================== c [1mFound solution: 1524608[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5726 | 31688 102087 | 10562 5653 383232 67.8 | 3.974 % | c | 5826 | 31688 102087 | 11618 5753 384170 66.8 | 3.984 % | c | 5976 | 31677 102063 | 12780 5901 387603 65.7 | 4.027 % | c ============================================================================== c [1mFound solution: 1518848[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6078 | 31699 102117 | 10566 6003 389713 64.9 | 4.027 % | c | 6178 | 31699 102117 | 11622 6103 402553 66.0 | 4.037 % | c | 6330 | 31699 102117 | 12784 6255 405201 64.8 | 4.037 % | c | 6555 | 31699 102117 | 14063 6480 426150 65.8 | 4.037 % | c | 6895 | 31656 101968 | 15469 6812 459916 67.5 | 4.080 % | c | 7401 | 31640 101929 | 17016 7316 506490 69.2 | 4.138 % | c | 8160 | 31640 101929 | 18718 8075 572320 70.9 | 4.138 % | c ============================================================================== c [1mFound solution: 1517568[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9071 | 31652 101961 | 10550 8985 664695 74.0 | 4.138 % | c | 9171 | 31652 101961 | 11605 9085 666938 73.4 | 4.177 % | c | 9322 | 31652 101961 | 12765 9236 686356 74.3 | 4.177 % | c | 9548 | 31641 101937 | 14042 9461 696613 73.6 | 4.221 % | c | 9886 | 31641 101937 | 15446 9799 734384 74.9 | 4.221 % | c | 10392 | 31611 101870 | 16990 10301 781995 75.9 | 4.350 % | c | 11151 | 31611 101870 | 18689 11060 858090 77.6 | 4.350 % | c ============================================================================== c [1mFound solution: 1509888[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11735 | 31632 101923 | 10544 11644 936880 80.5 | 4.350 % | c | 11836 | 31632 101923 | 11598 5923 443128 74.8 | 4.360 % | c | 11986 | 31632 101923 | 12758 6073 456585 75.2 | 4.360 % | c | 12212 | 31632 101923 | 14034 6299 491256 78.0 | 4.360 % | c | 12549 | 31632 101923 | 15437 6636 503437 75.9 | 4.360 % | c | 13055 | 31632 101923 | 16981 7142 583352 81.7 | 4.360 % | c | 13816 | 31605 101826 | 18679 7900 658907 83.4 | 4.375 % | c ============================================================================== c [1mFound solution: 1462528[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13891 | 31629 101884 | 10543 7975 665132 83.4 | 4.375 % | c | 13992 | 31594 101803 | 11597 8072 675547 83.7 | 4.513 % | c | 14143 | 31594 101803 | 12757 8223 678501 82.5 | 4.513 % | c | 14370 | 31594 101803 | 14032 8450 700849 82.9 | 4.513 % | c | 14707 | 31594 101803 | 15436 8787 737874 84.0 | 4.513 % | c | 15213 | 31594 101803 | 16979 9293 810649 87.2 | 4.513 % | c | 15974 | 31568 101734 | 18677 10048 902841 89.9 | 4.570 % | c | 17115 | 31479 101485 | 20545 11176 1000404 89.5 | 4.828 % | c | 18823 | 31461 101440 | 22599 12865 1179286 91.7 | 4.885 % | c ============================================================================== c [1mFound solution: 1459328[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20846 | 31466 101450 | 10488 14878 1319253 88.7 | 4.885 % | c | 20947 | 31466 101450 | 11536 7540 475839 63.1 | 4.966 % | c | 21098 | 31466 101450 | 12690 7691 494129 64.2 | 4.966 % | c | 21323 | 31466 101450 | 13959 7916 502860 63.5 | 4.966 % | c | 21665 | 31466 101450 | 15355 8258 524942 63.6 | 4.966 % | c | 22172 | 31466 101450 | 16891 8765 605766 69.1 | 4.966 % | c | 22931 | 31445 101403 | 18580 9522 697081 73.2 | 5.052 % | c | 24073 | 31427 101364 | 20438 10662 798004 74.8 | 5.123 % | c | 25782 | 31427 101364 | 22481 12371 1035789 83.7 | 5.123 % | c ============================================================================== c [1mFound solution: 1435008[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27602 | 31434 101367 | 10478 14188 1191101 84.0 | 5.123 % | c | 27706 | 31434 101367 | 11525 7198 525874 73.1 | 5.174 % | c | 27857 | 31434 101367 | 12678 7349 535217 72.8 | 5.174 % | c | 28082 | 31434 101367 | 13946 7574 563543 74.4 | 5.174 % | c | 28420 | 31405 101303 | 15340 7907 587243 74.3 | 5.302 % | c | 28927 | 31405 101303 | 16874 8414 653045 77.6 | 5.302 % | c | 29687 | 31405 101303 | 18562 9174 714479 77.9 | 5.302 % | c | 30826 | 31380 101242 | 20418 10307 854322 82.9 | 5.417 % | c | 32534 | 31353 101147 | 22460 12012 1062524 88.5 | 5.446 % | c | 35097 | 31353 101147 | 24706 14575 1401051 96.1 | 5.445 % | c ============================================================================== c [1mFound solution: 1424768[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38417 | 31375 101201 | 10458 17895 1877121 104.9 | 5.445 % | c | 38518 | 31375 101201 | 11503 9049 861399 95.2 | 5.454 % | c | 38672 | 31364 101177 | 12654 9200 886480 96.4 | 5.497 % | c | 38898 | 31343 101102 | 13919 9422 912731 96.9 | 5.511 % | c | 39239 | 31343 101102 | 15311 9763 926282 94.9 | 5.511 % | c | 39745 | 31343 101102 | 16842 10269 998183 97.2 | 5.511 % | c | 40504 | 31291 100937 | 18526 11020 1090759 99.0 | 5.611 % | c | 41644 | 31291 100937 | 20379 12160 1204458 99.1 | 5.611 % | c | 43352 | 31291 100937 | 22417 13868 1428447 103.0 | 5.611 % | c | 45915 | 31286 100922 | 24659 16425 1616181 98.4 | 5.625 % | c | 49759 | 31268 100863 | 27125 20265 1973613 97.4 | 5.654 % | c | 55527 | 31263 100848 | 29837 26030 2815258 108.2 | 5.668 % | c | 64177 | 31202 100673 | 32821 18908 1944788 102.9 | 5.825 % | c ============================================================================== c [1mFound solution: 1419008[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 67181 | 31230 100741 | 10410 21912 2405516 109.8 | 5.825 % | c | 67284 | 31203 100644 | 11451 5578 422494 75.7 | 5.846 % | c | 67435 | 31203 100644 | 12596 5729 447484 78.1 | 5.846 % | c | 67663 | 31181 100591 | 13855 5954 457168 76.8 | 5.932 % | c | 68001 | 31181 100591 | 15241 6292 519450 82.6 | 5.932 % | c | 68508 | 31181 100591 | 16765 6799 568748 83.7 | 5.932 % | c | 69272 | 31100 100306 | 18441 7549 638121 84.5 | 6.017 % | c | 70412 | 31100 100306 | 20286 8689 731156 84.1 | 6.017 % | c | 72122 | 31100 100306 | 22314 10399 969149 93.2 | 6.017 % | c | 74686 | 31063 100224 | 24546 12955 1268954 98.0 | 6.174 % | c | 78530 | 31052 100200 | 27000 16797 1605700 95.6 | 6.217 % | c | 84297 | 30861 99720 | 29700 22542 2247613 99.7 | 6.930 % | c | 92947 | 30784 99505 | 32671 31175 3241750 104.0 | 7.158 % | c | 105921 | 30635 98984 | 35938 24584 2712666 110.3 | 7.358 % | c | 125383 | 30535 98701 | 39531 23565 2441955 103.6 | 7.629 % | c | 154579 | 30491 98601 | 43485 27859 3077771 110.5 | 7.786 % | c ============================================================================== c [1mFound solution: 1408128[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 181498 | 30474 98559 | 10158 27308 2501698 91.6 | 7.786 % | c | 181599 | 30474 98559 | 11173 6928 259313 37.4 | 7.963 % | c | 181749 | 30474 98559 | 12291 7078 282906 40.0 | 7.963 % | c | 181974 | 30474 98559 | 13520 7303 308135 42.2 | 7.963 % | c | 182313 | 30474 98559 | 14872 7642 353208 46.2 | 7.963 % | c | 182825 | 30474 98559 | 16359 8154 420914 51.6 | 7.963 % | c | 183589 | 30474 98559 | 17995 8918 518007 58.1 | 7.963 % | c | 184728 | 30474 98559 | 19795 10057 662739 65.9 | 7.963 % | c | 186437 | 30474 98559 | 21774 11766 873251 74.2 | 7.963 % | c | 188999 | 30463 98526 | 23952 14327 1242894 86.8 | 7.991 % | c | 192844 | 30463 98526 | 26347 18172 1737435 95.6 | 7.991 % | c | 198610 | 30463 98526 | 28981 23938 2530725 105.7 | 7.991 % | c | 207260 | 30357 98178 | 31880 17155 1579892 92.1 | 8.219 % | c | 220239 | 30251 97839 | 35068 30111 3210953 106.6 | 8.433 % | c | 239703 | 30251 97839 | 38574 26455 2695906 101.9 | 8.433 % | c | 268895 | 30251 97839 | 42432 30474 3344315 109.7 | 8.433 % | c | 312686 | 30220 97756 | 46675 22390 1823582 81.4 | 8.519 % | c | 378370 | 30220 97756 | 51343 21306 1884108 88.4 | 8.519 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.85 0.94 0.90 2/56 18443 Raw data (stat): 18443 (runsolver) R 18442 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 426570483 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.99967 s] Raw data (loadavg): 0.87 0.94 0.90 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 1759 0 0 0 995 4 0 0 25 0 1 0 426570483 8568832 1690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2092 1690 603 41 0 2051 0 vsize: 8368 [startup+20.0005 s] Raw data (loadavg): 0.89 0.94 0.90 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2319 0 0 0 1994 5 0 0 25 0 1 0 426570483 10862592 2250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2652 2250 603 41 0 2611 0 vsize: 10608 [startup+30.0013 s] Raw data (loadavg): 0.91 0.94 0.90 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2564 0 0 0 2993 6 0 0 25 0 1 0 426570483 11923456 2495 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2911 2495 603 41 0 2870 0 vsize: 11644 [startup+40.0021 s] Raw data (loadavg): 0.92 0.94 0.90 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2746 0 0 0 3992 7 0 0 25 0 1 0 426570483 12595200 2677 4294967295 134512640 134672761 3221224544 3221223736 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3075 2677 603 41 0 3034 0 vsize: 12300 [startup+50.0029 s] Raw data (loadavg): 0.93 0.94 0.90 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2746 0 0 0 4993 7 0 0 25 0 1 0 426570483 12595200 2677 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3075 2677 603 41 0 3034 0 vsize: 12300 [startup+60.0031 s] Raw data (loadavg): 0.94 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2746 0 0 0 5992 7 0 0 25 0 1 0 426570483 12595200 2677 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3075 2677 603 41 0 3034 0 vsize: 12300 [startup+70.0035 s] Raw data (loadavg): 0.95 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 3282 0 0 0 6991 8 0 0 25 0 1 0 426570483 14905344 3213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3639 3213 603 41 0 3598 0 vsize: 14556 [startup+80.0041 s] Raw data (loadavg): 0.96 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 3395 0 0 0 7990 9 0 0 25 0 1 0 426570483 15310848 3326 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3738 3326 603 41 0 3697 0 vsize: 14952 [startup+90.0049 s] Raw data (loadavg): 0.96 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 3395 0 0 0 8990 9 0 0 25 0 1 0 426570483 15310848 3326 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3738 3326 603 41 0 3697 0 vsize: 14952 [startup+100.005 s] Raw data (loadavg): 0.97 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 3855 0 0 0 9990 10 0 0 25 0 1 0 426570483 17166336 3786 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4191 3786 603 41 0 4150 0 vsize: 16764 [startup+110.004 s] Raw data (loadavg): 0.97 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 4505 0 0 0 10988 11 0 0 25 0 1 0 426570483 19857408 4436 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4848 4436 603 41 0 4807 0 vsize: 19392 [startup+120.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 4884 0 0 0 11988 11 0 0 25 0 1 0 426570483 21467136 4815 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5241 4815 603 41 0 5200 0 vsize: 20964 [startup+130.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 12987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5568 5163 603 41 0 5527 0 vsize: 22272 [startup+140.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 13987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5568 5163 603 41 0 5527 0 vsize: 22272 [startup+150.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 14987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5568 5163 603 41 0 5527 0 vsize: 22272 [startup+160.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 15987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5568 5163 603 41 0 5527 0 vsize: 22272 [startup+170.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 16987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5568 5163 603 41 0 5527 0 vsize: 22272 [startup+180.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 17988 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5568 5163 603 41 0 5527 0 vsize: 22272 [startup+190.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 18988 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5568 5163 603 41 0 5527 0 vsize: 22272 [startup+200.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 19988 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5568 5163 603 41 0 5527 0 vsize: 22272 [startup+210.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5351 0 0 0 20988 13 0 0 25 0 1 0 426570483 23474176 5282 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5731 5282 603 41 0 5690 0 vsize: 22924 [startup+220.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 21987 14 0 0 25 0 1 0 426570483 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6124 5689 603 41 0 6083 0 vsize: 24496 [startup+230.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18443 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 22987 14 0 0 25 0 1 0 426570483 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6124 5689 603 41 0 6083 0 vsize: 24496 [startup+240.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18498 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 23987 14 0 0 25 0 1 0 426570483 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6124 5689 603 41 0 6083 0 vsize: 24496 [startup+250.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/56 18498 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 24988 14 0 0 25 0 1 0 426570483 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6124 5689 603 41 0 6083 0 vsize: 24496 [startup+260.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 18498 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 25988 14 0 0 25 0 1 0 426570483 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6124 5689 603 41 0 6083 0 vsize: 24496 [startup+270.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 18498 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5872 0 0 0 26988 14 0 0 25 0 1 0 426570483 25485312 5803 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6222 5803 603 41 0 6181 0 vsize: 24888 [startup+280.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 18498 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6411 0 0 0 27986 16 0 0 25 0 1 0 426570483 27758592 6342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6777 6342 603 41 0 6736 0 vsize: 27108 [startup+290.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 18498 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 28986 16 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6909 6460 603 41 0 6868 0 vsize: 27636 [startup+300.005 s] Raw data (loadavg): 1.07 0.99 0.91 2/56 18500 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 29986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6909 6460 603 41 0 6868 0 vsize: 27636 [startup+310.005 s] Raw data (loadavg): 1.06 0.99 0.91 2/56 18500 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 30986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6909 6460 603 41 0 6868 0 vsize: 27636 [startup+320.005 s] Raw data (loadavg): 1.05 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 31986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6909 6460 603 41 0 6868 0 vsize: 27636 [startup+330.005 s] Raw data (loadavg): 1.04 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 32986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6909 6460 603 41 0 6868 0 vsize: 27636 [startup+340.005 s] Raw data (loadavg): 1.03 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 33986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6909 6460 603 41 0 6868 0 vsize: 27636 [startup+350.006 s] Raw data (loadavg): 1.03 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6959 0 0 0 34985 18 0 0 25 0 1 0 426570483 30044160 6890 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7335 6890 603 41 0 7294 0 vsize: 29340 [startup+360.006 s] Raw data (loadavg): 1.02 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 35984 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7071 603 41 0 7457 0 vsize: 29992 [startup+370.006 s] Raw data (loadavg): 1.02 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 36985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7071 603 41 0 7457 0 vsize: 29992 [startup+380.006 s] Raw data (loadavg): 1.02 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 37985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7071 603 41 0 7457 0 vsize: 29992 [startup+390.007 s] Raw data (loadavg): 1.01 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 38985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7071 603 41 0 7457 0 vsize: 29992 [startup+400.007 s] Raw data (loadavg): 1.01 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 39985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7071 603 41 0 7457 0 vsize: 29992 [startup+410.007 s] Raw data (loadavg): 1.01 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 40985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223692 134565030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7071 603 41 0 7457 0 vsize: 29992 [startup+420.008 s] Raw data (loadavg): 1.01 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 41986 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7071 603 41 0 7457 0 vsize: 29992 [startup+430.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 42986 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7071 603 41 0 7457 0 vsize: 29992 [startup+440.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7141 0 0 0 43986 19 0 0 25 0 1 0 426570483 30711808 7072 4294967295 134512640 134672761 3221224544 3221223728 134559575 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7072 603 41 0 7457 0 vsize: 29992 [startup+450.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7142 0 0 0 44986 19 0 0 25 0 1 0 426570483 30711808 7073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7073 603 41 0 7457 0 vsize: 29992 [startup+460.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 45986 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+470.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 46986 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+480.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 47986 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+490.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 48987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+500.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 49987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+510.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 50987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+520.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 51987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+530.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18502 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 52987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+540.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 53986 20 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+550.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 54986 20 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+560.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 55986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+570.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 56986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+580.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 57986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+590.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 58986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+600.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 59986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+610.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 60986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7074 603 41 0 7457 0 vsize: 29992 [startup+620.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 61986 21 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+630.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 62986 21 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+640.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 63986 21 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+650.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 64986 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+660.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 65986 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+670.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 66987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+680.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 67986 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+690.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 68987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+700.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 69987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+710.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 70987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134560285 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+720.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 71987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+730.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 72987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+740.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 73987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+750.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 74987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+760.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 75988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+770.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 76988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+780.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 77988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+790.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 78988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+800.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 79988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+810.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 80988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+820.016 s] Raw data (loadavg): 1.00 0.99 0.91 3/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 81989 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+830.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18504 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 82989 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7498 7075 603 41 0 7457 0 vsize: 29992 [startup+840.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7227 0 0 0 83988 23 0 0 25 0 1 0 426570483 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7596 7158 603 41 0 7555 0 vsize: 30384 [startup+850.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7227 0 0 0 84989 23 0 0 25 0 1 0 426570483 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7596 7158 603 41 0 7555 0 vsize: 30384 [startup+860.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7227 0 0 0 85989 23 0 0 25 0 1 0 426570483 31113216 7158 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7596 7158 603 41 0 7555 0 vsize: 30384 [startup+870.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7227 0 0 0 86989 23 0 0 25 0 1 0 426570483 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7596 7158 603 41 0 7555 0 vsize: 30384 [startup+880.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7230 0 0 0 87989 23 0 0 25 0 1 0 426570483 31113216 7161 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7596 7161 603 41 0 7555 0 vsize: 30384 [startup+890.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7245 0 0 0 88989 23 0 0 25 0 1 0 426570483 31248384 7176 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7629 7176 603 41 0 7588 0 vsize: 30516 [startup+900.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7277 0 0 0 89989 23 0 0 25 0 1 0 426570483 31412224 7208 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7669 7208 603 41 0 7628 0 vsize: 30676 [startup+910.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7294 0 0 0 90990 23 0 0 25 0 1 0 426570483 31412224 7225 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7669 7225 603 41 0 7628 0 vsize: 30676 [startup+920.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7304 0 0 0 91990 23 0 0 25 0 1 0 426570483 31576064 7235 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7709 7235 603 41 0 7668 0 vsize: 30836 [startup+930.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7319 0 0 0 92990 23 0 0 25 0 1 0 426570483 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7709 7250 603 41 0 7668 0 vsize: 30836 [startup+940.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7319 0 0 0 93990 23 0 0 25 0 1 0 426570483 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7709 7250 603 41 0 7668 0 vsize: 30836 [startup+950.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7319 0 0 0 94990 23 0 0 25 0 1 0 426570483 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7709 7250 603 41 0 7668 0 vsize: 30836 [startup+960.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7319 0 0 0 95990 23 0 0 25 0 1 0 426570483 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7709 7250 603 41 0 7668 0 vsize: 30836 [startup+970.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7329 0 0 0 96990 23 0 0 25 0 1 0 426570483 31576064 7260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7709 7260 603 41 0 7668 0 vsize: 30836 [startup+980.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7342 0 0 0 97990 24 0 0 25 0 1 0 426570483 31739904 7273 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7749 7273 603 41 0 7708 0 vsize: 30996 [startup+990.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7351 0 0 0 98990 24 0 0 25 0 1 0 426570483 31739904 7282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7749 7282 603 41 0 7708 0 vsize: 30996 [startup+1000.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7356 0 0 0 99990 24 0 0 25 0 1 0 426570483 31739904 7287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7749 7287 603 41 0 7708 0 vsize: 30996 [startup+1010.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7377 0 0 0 100990 24 0 0 25 0 1 0 426570483 31887360 7308 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7785 7308 603 41 0 7744 0 vsize: 31140 [startup+1020.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7390 0 0 0 101989 24 0 0 25 0 1 0 426570483 32047104 7321 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7824 7321 603 41 0 7783 0 vsize: 31296 [startup+1030.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7390 0 0 0 102989 25 0 0 25 0 1 0 426570483 32047104 7321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7824 7321 603 41 0 7783 0 vsize: 31296 [startup+1040.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7469 0 0 0 103989 25 0 0 25 0 1 0 426570483 32313344 7400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7889 7400 603 41 0 7848 0 vsize: 31556 [startup+1050.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7960 0 0 0 104987 27 0 0 25 0 1 0 426570483 34299904 7891 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8374 7891 603 41 0 8333 0 vsize: 33496 [startup+1060.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 105986 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8227 603 41 0 8659 0 vsize: 34800 [startup+1070.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 106987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8227 603 41 0 8659 0 vsize: 34800 [startup+1080.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 107987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8227 603 41 0 8659 0 vsize: 34800 [startup+1090.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 108987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8227 603 41 0 8659 0 vsize: 34800 [startup+1100.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 109987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8227 603 41 0 8659 0 vsize: 34800 [startup+1110.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 110987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8227 603 41 0 8659 0 vsize: 34800 [startup+1120.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 111988 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8227 603 41 0 8659 0 vsize: 34800 [startup+1130.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18506 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 112988 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8227 603 41 0 8659 0 vsize: 34800 [startup+1140.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18508 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8300 0 0 0 113988 28 0 0 25 0 1 0 426570483 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8231 603 41 0 8659 0 vsize: 34800 [startup+1150.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18508 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8300 0 0 0 114988 28 0 0 25 0 1 0 426570483 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8231 603 41 0 8659 0 vsize: 34800 [startup+1160.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18508 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8300 0 0 0 115988 28 0 0 25 0 1 0 426570483 35635200 8231 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8231 603 41 0 8659 0 vsize: 34800 [startup+1170.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18508 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8300 0 0 0 116989 28 0 0 25 0 1 0 426570483 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8700 8231 603 41 0 8659 0 vsize: 34800 [startup+1180.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18508 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8334 0 0 0 117989 28 0 0 25 0 1 0 426570483 35897344 8265 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8764 8265 603 41 0 8723 0 vsize: 35056 [startup+1190.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18508 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8473 0 0 0 118988 28 0 0 25 0 1 0 426570483 36438016 8404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8896 8404 603 41 0 8855 0 vsize: 35584 [startup+1200.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/56 18508 Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8473 0 0 0 119988 28 0 0 25 0 1 0 426570483 36438016 8404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8896 8404 603 41 0 8855 0 vsize: 35584 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 1.00 0.99 0.91 1/56 18508 Raw data (stat): 18443 (minisat+) Z 18442 12452 12451 0 -1 12 8476 0 0 0 119988 30 0 0 25 0 1 0 426570483 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.05 CPU time (s): 1200.19 CPU user time (s): 1199.89 CPU system time (s): 0.302953 CPU usage (%): 100.012 Max. virtual memory (Kb): 35584 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####