Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-gr4x6.opb |
MD5SUM | c1c7537cd9b3e10215a81ec1ca3be5cb |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2605440 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 504 |
Biggest coefficient in the objective function | 148373504 |
Number of bits for the biggest coefficient in the objective function | 28 |
Sum of the numbers in the objective function | 3393589600 |
Number of bits of the sum of numbers in the objective function | 32 |
Biggest number in a constraint | 148373504 |
Number of bits of the biggest number in a constraint | 28 |
Biggest sum of numbers in a constraint | 3393589600 |
Number of bits of the biggest sum of numbers | 32 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 504 |
Total number of constraints | 34 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 34 |
Minimum length of a constraint | 21 |
Maximum length of a constraint | 120 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc26 THE 2005-04-21 12:23:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18985 boxname=wulflinc26 idbench=1461 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: c1c7537cd9b3e10215a81ec1ca3be5cb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-gr4x6.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-gr4x6.opb IDLAUNCH: 18985 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 537328 kB Buffers: 28072 kB Cached: 438952 kB SwapCached: 68 kB Active: 55720 kB Inactive: 414196 kB HighTotal: 131008 kB HighFree: 1428 kB LowTotal: 903652 kB LowFree: 535900 kB SwapTotal: 2097892 kB SwapFree: 2097800 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6876 kB Slab: 21692 kB Committed_AS: 63712 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 12:43:50 (client local time) WITH STATUS 10 IN 1200.32 SECONDS stats: 18985 7 1200.32 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 44 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########## c -- Clauses(.)/Splits(s): (none) c ---[ 42]---> Sorter-cost: 972 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 972 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 900 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 888 Base: 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 471 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 359 Base: 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 359 Base: 2 2 2 2 2 2 2 2 2 c ---[ 23]---> BDD-cost: 19 c ---[ 22]---> BDD-cost: 16 c ---[ 21]---> BDD-cost: 13 c ---[ 20]---> BDD-cost: 13 c ---[ 19]---> BDD-cost: 15 c ---[ 18]---> BDD-cost: 15 c ---[ 17]---> BDD-cost: 15 c ---[ 16]---> BDD-cost: 15 c ---[ 15]---> BDD-cost: 13 c ---[ 14]---> BDD-cost: 13 c ---[ 13]---> BDD-cost: 15 c ---[ 12]---> BDD-cost: 15 c ---[ 11]---> BDD-cost: 17 c ---[ 10]---> BDD-cost: 15 c ---[ 9]---> BDD-cost: 15 c ---[ 8]---> BDD-cost: 13 c ---[ 7]---> BDD-cost: 13 c ---[ 6]---> BDD-cost: 15 c ---[ 5]---> BDD-cost: 13 c ---[ 4]---> BDD-cost: 13 c ---[ 3]---> BDD-cost: 19 c ---[ 2]---> BDD-cost: 16 c ---[ 1]---> BDD-cost: 17 c ---[ 0]---> BDD-cost: 15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 15349 36385 | 5116 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 5885984[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:63755 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 78 | 192309 449611 | 64103 78 360 4.6 | 0.000 % | c | 179 | 192309 449611 | 70513 179 1995 11.1 | 0.939 % | c | 330 | 192309 449611 | 77564 330 2915 8.8 | 0.939 % | c | 555 | 192309 449611 | 85321 555 4340 7.8 | 0.939 % | c | 892 | 192309 449611 | 93853 892 6726 7.5 | 0.939 % | c | 1399 | 192309 449611 | 103238 1399 14459 10.3 | 0.939 % | c | 2158 | 192215 449400 | 113562 2155 30502 14.2 | 0.975 % | c | 3297 | 192215 449400 | 124918 3294 177563 53.9 | 0.975 % | c ============================================================================== c [1mFound solution: 4547392[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3400 | 192789 451295 | 64263 3389 179355 52.9 | 0.975 % | c | 3500 | 192789 451295 | 70689 3489 184974 53.0 | 1.010 % | c | 3651 | 192769 451250 | 77758 3639 186369 51.2 | 1.017 % | c | 3876 | 192357 450318 | 85534 3857 190287 49.3 | 1.191 % | c ============================================================================== c [1mFound solution: 4505992[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4161 | 192378 450633 | 64126 4129 197031 47.7 | 1.191 % | c | 4261 | 192378 450633 | 70538 4229 198431 46.9 | 1.360 % | c | 4411 | 192279 450409 | 77592 4377 200682 45.8 | 1.402 % | c | 4636 | 192244 450331 | 85351 4599 203524 44.3 | 1.417 % | c | 4973 | 192244 450331 | 93886 4936 248916 50.4 | 1.417 % | c | 5480 | 192244 450331 | 103275 5443 257646 47.3 | 1.417 % | c | 6239 | 192244 450331 | 113603 6202 282898 45.6 | 1.417 % | c | 7379 | 192111 450029 | 124963 7106 316426 44.5 | 1.473 % | c | 9089 | 191828 449383 | 137459 8807 401005 45.5 | 1.593 % | c | 11653 | 191808 449338 | 151205 11369 430975 37.9 | 1.600 % | c | 15499 | 191615 448906 | 166326 15206 784188 51.6 | 1.684 % | c ============================================================================== c [1mFound solution: 3607624[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16365 | 191688 449214 | 63896 16043 812376 50.6 | 1.684 % | c ============================================================================== c [1mFound solution: 3423277[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16372 | 191727 449409 | 63909 16050 812415 50.6 | 1.684 % | c | 16472 | 191727 449409 | 70299 16150 822793 50.9 | 1.805 % | c | 16622 | 191727 449409 | 77329 16300 832150 51.1 | 1.805 % | c | 16847 | 191727 449409 | 85062 16525 848482 51.3 | 1.805 % | c | 17185 | 191727 449409 | 93569 16863 864612 51.3 | 1.805 % | c | 17691 | 191727 449409 | 102926 17369 939920 54.1 | 1.805 % | c | 18450 | 191663 449264 | 113218 18127 990313 54.6 | 1.830 % | c ============================================================================== c [1mFound solution: 3400032[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19266 | 191676 449301 | 63892 18943 1179458 62.3 | 1.830 % | c | 19367 | 191588 449103 | 70281 19024 1183836 62.2 | 1.871 % | c | 19518 | 191416 448715 | 77309 19149 1190402 62.2 | 1.954 % | c | 19744 | 191368 448606 | 85040 19374 1203086 62.1 | 1.975 % | c | 20082 | 191368 448606 | 93544 19712 1240205 62.9 | 1.975 % | c | 20591 | 191368 448606 | 102898 20221 1291193 63.9 | 1.975 % | c | 21351 | 190404 446406 | 113188 20892 1335676 63.9 | 2.419 % | c | 22490 | 190404 446406 | 124507 22031 1452208 65.9 | 2.419 % | c | 24198 | 190404 446406 | 136958 23739 1636081 68.9 | 2.419 % | c ============================================================================== c [1mFound solution: 3367610[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24649 | 190424 446476 | 63474 24181 1665305 68.9 | 2.419 % | c ============================================================================== c [1mFound solution: 3298476[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24667 | 190445 446527 | 63481 24199 1665514 68.8 | 2.419 % | c | 24767 | 190445 446527 | 69829 24299 1677707 69.0 | 2.422 % | c | 24917 | 190445 446527 | 76812 24449 1680953 68.8 | 2.422 % | c | 25143 | 190445 446527 | 84493 24675 1700084 68.9 | 2.422 % | c | 25480 | 190445 446527 | 92942 25012 1704985 68.2 | 2.422 % | c | 25988 | 190445 446527 | 102236 25520 1713199 67.1 | 2.422 % | c | 26747 | 190445 446527 | 112460 26279 1847940 70.3 | 2.422 % | c | 27886 | 190408 446443 | 123706 27412 2018790 73.6 | 2.440 % | c | 29595 | 190388 446399 | 136077 29115 2098475 72.1 | 2.448 % | c ============================================================================== c [1mFound solution: 3268695[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30664 | 190409 446461 | 63469 30181 2278674 75.5 | 2.448 % | c | 30764 | 190409 446461 | 69815 30281 2280211 75.3 | 2.457 % | c | 30915 | 190409 446461 | 76797 30432 2286100 75.1 | 2.457 % | c | 31141 | 190409 446461 | 84477 30658 2295700 74.9 | 2.457 % | c | 31478 | 190409 446461 | 92924 30995 2327171 75.1 | 2.457 % | c ============================================================================== c [1mFound solution: 3134720[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31735 | 190420 446494 | 63473 31252 2353209 75.3 | 2.457 % | c | 31835 | 190379 446400 | 69820 31351 2358121 75.2 | 2.475 % | c | 31986 | 190379 446400 | 76802 31502 2369464 75.2 | 2.475 % | c | 32211 | 190379 446400 | 84482 31727 2395563 75.5 | 2.475 % | c | 32550 | 190379 446400 | 92930 32066 2438868 76.1 | 2.475 % | c | 33056 | 190379 446400 | 102223 32572 2483971 76.3 | 2.475 % | c | 33817 | 190379 446400 | 112446 33333 2627192 78.8 | 2.475 % | c | 34956 | 190379 446400 | 123690 34472 2710906 78.6 | 2.475 % | c | 36664 | 190317 446259 | 136060 36177 2807464 77.6 | 2.502 % | c | 39226 | 190317 446259 | 149666 38739 3106741 80.2 | 2.502 % | c | 43070 | 190317 446259 | 164632 42583 3440355 80.8 | 2.502 % | c | 48838 | 190110 445788 | 181095 48336 3908973 80.9 | 2.592 % | c | 57487 | 190110 445788 | 199205 56985 4842937 85.0 | 2.592 % | c | 70462 | 190110 445788 | 219126 69960 5996043 85.7 | 2.592 % | c ============================================================================== c [1mFound solution: 3127040[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 80923 | 190122 445817 | 63374 80421 6986009 86.9 | 2.592 % | c | 81023 | 190122 445817 | 69711 21093 1212194 57.5 | 2.593 % | c | 81173 | 190122 445817 | 76682 21243 1225608 57.7 | 2.593 % | c | 81398 | 190122 445817 | 84350 21468 1245486 58.0 | 2.593 % | c | 81739 | 190122 445817 | 92785 21809 1271020 58.3 | 2.593 % | c | 82247 | 190122 445817 | 102064 22317 1310224 58.7 | 2.593 % | c | 83007 | 190122 445817 | 112270 23077 1358767 58.9 | 2.593 % | c | 84146 | 190122 445817 | 123497 24216 1430249 59.1 | 2.593 % | c | 85854 | 190122 445817 | 135847 25924 1605179 61.9 | 2.593 % | c ============================================================================== c [1mFound solution: 3059840[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86384 | 190155 445901 | 63385 26454 1655034 62.6 | 2.593 % | c | 86484 | 190155 445901 | 69723 26554 1660764 62.5 | 2.593 % | c | 86636 | 190155 445901 | 76695 26706 1670505 62.6 | 2.593 % | c | 86863 | 190155 445901 | 84365 26933 1691632 62.8 | 2.593 % | c | 87200 | 190155 445901 | 92801 27270 1713092 62.8 | 2.593 % | c | 87711 | 190148 445886 | 102082 27780 1742338 62.7 | 2.596 % | c | 88471 | 190148 445886 | 112290 28540 1794240 62.9 | 2.596 % | c | 89614 | 190148 445886 | 123519 29683 1899441 64.0 | 2.596 % | c | 91323 | 190148 445886 | 135871 31392 2052966 65.4 | 2.596 % | c | 93886 | 190148 445886 | 149458 33955 2331342 68.7 | 2.596 % | c | 97731 | 190148 445886 | 164404 37800 2635628 69.7 | 2.596 % | c | 103499 | 190042 445647 | 180844 43566 3104488 71.3 | 2.640 % | c ============================================================================== c [1mFound solution: 3058432[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 104294 | 190008 445577 | 63336 44357 3167623 71.4 | 2.640 % | c | 104398 | 190008 445577 | 69669 44461 3169160 71.3 | 2.660 % | c | 104548 | 190008 445577 | 76636 44611 3171196 71.1 | 2.660 % | c | 104774 | 190008 445577 | 84300 44837 3199431 71.4 | 2.660 % | c | 105111 | 190008 445577 | 92730 45174 3234046 71.6 | 2.660 % | c | 105617 | 190008 445577 | 102003 45680 3273663 71.7 | 2.660 % | c | 106376 | 190008 445577 | 112203 46439 3351421 72.2 | 2.660 % | c | 107516 | 190008 445577 | 123423 47579 3467405 72.9 | 2.660 % | c | 109224 | 190008 445577 | 135766 49287 3626707 73.6 | 2.660 % | c | 111787 | 190008 445577 | 149342 51850 3823598 73.7 | 2.660 % | c | 115633 | 190005 445570 | 164277 55664 4214129 75.7 | 2.663 % | c c *** TERMINATED *** s SATISFIABLE v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 X0_bit0 X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 X1_bit1 X1_bit2 X1_bit3 X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 X11_bit0 X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 X15_bit0 X15_bit1 X15_bit2 X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 X16_bit0 -X16_bit1 X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bi#### 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.79 0.92 0.90 2/54 31434 Raw data (stat): 31434 (runsolver) R 31433 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545058195 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.82 0.93 0.90 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 5920 0 0 0 984 14 0 0 25 0 1 0 545058195 30085120 5738 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7345 5738 603 41 0 7304 0 vsize: 29380 [startup+20.0012 s] Raw data (loadavg): 0.85 0.93 0.90 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 6142 0 0 0 1983 15 0 0 25 0 1 0 545058195 31395840 5960 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7665 5960 603 41 0 7624 0 vsize: 30660 [startup+30.0021 s] Raw data (loadavg): 0.87 0.93 0.90 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 6184 0 0 0 2983 15 0 0 25 0 1 0 545058195 31526912 6002 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7697 6002 603 41 0 7656 0 vsize: 30788 [startup+40.0022 s] Raw data (loadavg): 0.89 0.93 0.90 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 6286 0 0 0 3981 16 0 0 25 0 1 0 545058195 31928320 6104 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7795 6104 603 41 0 7754 0 vsize: 31180 [startup+50.0032 s] Raw data (loadavg): 0.91 0.93 0.90 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 6424 0 0 0 4981 16 0 0 25 0 1 0 545058195 32468992 6242 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7927 6242 603 41 0 7886 0 vsize: 31708 [startup+60.0029 s] Raw data (loadavg): 0.92 0.93 0.90 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 6603 0 0 0 5980 17 0 0 25 0 1 0 545058195 33275904 6421 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8124 6421 603 41 0 8083 0 vsize: 32496 [startup+70.0034 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 6763 0 0 0 6980 17 0 0 25 0 1 0 545058195 33943552 6581 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8287 6581 603 41 0 8246 0 vsize: 33148 [startup+80.0046 s] Raw data (loadavg): 0.94 0.94 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 6873 0 0 0 7979 17 0 0 25 0 1 0 545058195 34336768 6670 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8383 6670 603 41 0 8342 0 vsize: 33532 [startup+90.005 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 6997 0 0 0 8979 18 0 0 25 0 1 0 545058195 34734080 6794 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8480 6794 603 41 0 8439 0 vsize: 33920 [startup+100.005 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 7246 0 0 0 9978 18 0 0 25 0 1 0 545058195 35684352 7023 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8712 7023 603 41 0 8671 0 vsize: 34848 [startup+110.005 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 7318 0 0 0 10978 18 0 0 25 0 1 0 545058195 36081664 7095 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8809 7095 603 41 0 8768 0 vsize: 35236 [startup+120.006 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 7412 0 0 0 11978 19 0 0 25 0 1 0 545058195 36483072 7189 4294967295 134512640 134672761 3221224624 3221223768 134560555 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8907 7189 603 41 0 8866 0 vsize: 35628 [startup+130.005 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 7511 0 0 0 12978 19 0 0 25 0 1 0 545058195 36876288 7288 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9003 7288 603 41 0 8962 0 vsize: 36012 [startup+140.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 7582 0 0 0 13978 19 0 0 25 0 1 0 545058195 37142528 7359 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9068 7359 603 41 0 9027 0 vsize: 36272 [startup+150.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 7733 0 0 0 14978 20 0 0 25 0 1 0 545058195 37662720 7510 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9195 7510 603 41 0 9154 0 vsize: 36780 [startup+160.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 7833 0 0 0 15978 20 0 0 25 0 1 0 545058195 37945344 7569 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9264 7569 603 41 0 9223 0 vsize: 37056 [startup+170.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 7990 0 0 0 16978 20 0 0 25 0 1 0 545058195 38600704 7726 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9424 7726 603 41 0 9383 0 vsize: 37696 [startup+180.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8124 0 0 0 17977 21 0 0 25 0 1 0 545058195 39116800 7860 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9550 7860 603 41 0 9509 0 vsize: 38200 [startup+190.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8204 0 0 0 18978 21 0 0 25 0 1 0 545058195 39383040 7940 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9615 7940 603 41 0 9574 0 vsize: 38460 [startup+200.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8302 0 0 0 19977 21 0 0 25 0 1 0 545058195 39780352 8038 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9712 8038 603 41 0 9671 0 vsize: 38848 [startup+210.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8401 0 0 0 20977 21 0 0 25 0 1 0 545058195 40304640 8137 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9840 8137 603 41 0 9799 0 vsize: 39360 [startup+220.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8511 0 0 0 21977 22 0 0 25 0 1 0 545058195 40730624 8247 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9944 8247 603 41 0 9903 0 vsize: 39776 [startup+230.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8598 0 0 0 22977 22 0 0 25 0 1 0 545058195 40980480 8313 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10005 8313 603 41 0 9964 0 vsize: 40020 [startup+240.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8696 0 0 0 23977 23 0 0 25 0 1 0 545058195 41377792 8411 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10102 8411 603 41 0 10061 0 vsize: 40408 [startup+250.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8812 0 0 0 24976 23 0 0 25 0 1 0 545058195 42045440 8527 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10265 8527 603 41 0 10224 0 vsize: 41060 [startup+260.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 8924 0 0 0 25976 24 0 0 25 0 1 0 545058195 42450944 8639 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10364 8639 603 41 0 10323 0 vsize: 41456 [startup+270.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9015 0 0 0 26975 24 0 0 25 0 1 0 545058195 42844160 8730 4294967295 134512640 134672761 3221224624 3221223760 134565110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10460 8730 603 41 0 10419 0 vsize: 41840 [startup+280.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9153 0 0 0 27975 25 0 0 25 0 1 0 545058195 43384832 8868 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10592 8868 603 41 0 10551 0 vsize: 42368 [startup+290.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9286 0 0 0 28975 25 0 0 25 0 1 0 545058195 43917312 9001 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10722 9001 603 41 0 10681 0 vsize: 42888 [startup+300.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9403 0 0 0 29975 25 0 0 25 0 1 0 545058195 44449792 9118 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10852 9118 603 41 0 10811 0 vsize: 43408 [startup+310.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9514 0 0 0 30975 26 0 0 25 0 1 0 545058195 44847104 9229 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10949 9229 603 41 0 10908 0 vsize: 43796 [startup+320.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9615 0 0 0 31975 26 0 0 25 0 1 0 545058195 45248512 9330 4294967295 134512640 134672761 3221224624 3221223824 134557922 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11047 9330 603 41 0 11006 0 vsize: 44188 [startup+330.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9724 0 0 0 32975 26 0 0 25 0 1 0 545058195 45776896 9439 4294967295 134512640 134672761 3221224624 3221223760 134560634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11176 9439 603 41 0 11135 0 vsize: 44704 [startup+340.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9815 0 0 0 33974 27 0 0 25 0 1 0 545058195 46047232 9530 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11242 9530 603 41 0 11201 0 vsize: 44968 [startup+350.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 9937 0 0 0 34974 27 0 0 25 0 1 0 545058195 46563328 9652 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11368 9652 603 41 0 11327 0 vsize: 45472 [startup+360.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10056 0 0 0 35974 27 0 0 25 0 1 0 545058195 47095808 9771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11498 9771 603 41 0 11457 0 vsize: 45992 [startup+370.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10164 0 0 0 36974 27 0 0 25 0 1 0 545058195 47493120 9879 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11595 9879 603 41 0 11554 0 vsize: 46380 [startup+380.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10249 0 0 0 37974 27 0 0 25 0 1 0 545058195 47886336 9964 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11691 9964 603 41 0 11650 0 vsize: 46764 [startup+390.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10325 0 0 0 38974 28 0 0 25 0 1 0 545058195 48152576 10040 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11756 10040 603 41 0 11715 0 vsize: 47024 [startup+400.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10421 0 0 0 39974 28 0 0 25 0 1 0 545058195 48545792 10136 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11852 10136 603 41 0 11811 0 vsize: 47408 [startup+410.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10518 0 0 0 40974 29 0 0 25 0 1 0 545058195 48939008 10233 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11948 10233 603 41 0 11907 0 vsize: 47792 [startup+420.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10606 0 0 0 41974 29 0 0 25 0 1 0 545058195 49340416 10321 4294967295 134512640 134672761 3221224624 3221223728 134560303 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12046 10321 603 41 0 12005 0 vsize: 48184 [startup+430.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10702 0 0 0 42974 29 0 0 25 0 1 0 545058195 49709056 10417 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12136 10417 603 41 0 12095 0 vsize: 48544 [startup+440.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10794 0 0 0 43973 30 0 0 25 0 1 0 545058195 50085888 10509 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12228 10509 603 41 0 12187 0 vsize: 48912 [startup+450.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10885 0 0 0 44973 30 0 0 25 0 1 0 545058195 50483200 10600 4294967295 134512640 134672761 3221224624 3221223728 134560313 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12325 10600 603 41 0 12284 0 vsize: 49300 [startup+460.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 10985 0 0 0 45972 31 0 0 25 0 1 0 545058195 50872320 10700 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12420 10700 603 41 0 12379 0 vsize: 49680 [startup+470.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11110 0 0 0 46972 31 0 0 25 0 1 0 545058195 51388416 10825 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12546 10825 603 41 0 12505 0 vsize: 50184 [startup+480.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11211 0 0 0 47972 32 0 0 25 0 1 0 545058195 51789824 10926 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12644 10926 603 41 0 12603 0 vsize: 50576 [startup+490.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11278 0 0 0 48972 32 0 0 25 0 1 0 545058195 52056064 10993 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12709 10993 603 41 0 12668 0 vsize: 50836 [startup+500.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11382 0 0 0 49972 32 0 0 25 0 1 0 545058195 52453376 11097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12806 11097 603 41 0 12765 0 vsize: 51224 [startup+510.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11482 0 0 0 50971 33 0 0 25 0 1 0 545058195 52842496 11197 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12901 11197 603 41 0 12860 0 vsize: 51604 [startup+520.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11578 0 0 0 51971 33 0 0 25 0 1 0 545058195 53223424 11293 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12994 11293 603 41 0 12953 0 vsize: 51976 [startup+530.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11657 0 0 0 52971 34 0 0 25 0 1 0 545058195 53616640 11372 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13090 11372 603 41 0 13049 0 vsize: 52360 [startup+540.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11740 0 0 0 53970 34 0 0 25 0 1 0 545058195 53878784 11455 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13154 11455 603 41 0 13113 0 vsize: 52616 [startup+550.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11835 0 0 0 54970 34 0 0 25 0 1 0 545058195 54267904 11550 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13249 11550 603 41 0 13208 0 vsize: 52996 [startup+560.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11904 0 0 0 55970 35 0 0 25 0 1 0 545058195 54530048 11619 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13313 11619 603 41 0 13272 0 vsize: 53252 [startup+570.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 11982 0 0 0 56970 35 0 0 25 0 1 0 545058195 54923264 11697 4294967295 134512640 134672761 3221224624 3221223792 134561275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13409 11697 603 41 0 13368 0 vsize: 53636 [startup+580.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12049 0 0 0 57970 35 0 0 25 0 1 0 545058195 55185408 11764 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13473 11764 603 41 0 13432 0 vsize: 53892 [startup+590.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12125 0 0 0 58971 35 0 0 25 0 1 0 545058195 55439360 11840 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13535 11840 603 41 0 13494 0 vsize: 54140 [startup+600.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12195 0 0 0 59971 36 0 0 25 0 1 0 545058195 56094720 11910 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13695 11910 603 41 0 13654 0 vsize: 54780 [startup+610.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12278 0 0 0 60971 36 0 0 25 0 1 0 545058195 56360960 11993 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13760 11993 603 41 0 13719 0 vsize: 55040 [startup+620.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12355 0 0 0 61972 36 0 0 25 0 1 0 545058195 56623104 12070 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13824 12070 603 41 0 13783 0 vsize: 55296 [startup+630.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12428 0 0 0 62982 36 0 0 25 0 1 0 545058195 57020416 12143 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13921 12143 603 41 0 13880 0 vsize: 55684 [startup+640.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12505 0 0 0 63982 37 0 0 25 0 1 0 545058195 57282560 12220 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13985 12220 603 41 0 13944 0 vsize: 55940 [startup+650.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12581 0 0 0 64982 37 0 0 25 0 1 0 545058195 57544704 12296 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14049 12296 603 41 0 14008 0 vsize: 56196 [startup+660.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12658 0 0 0 65980 37 0 0 25 0 1 0 545058195 57929728 12373 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14143 12373 603 41 0 14102 0 vsize: 56572 [startup+670.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12727 0 0 0 66981 38 0 0 25 0 1 0 545058195 58208256 12442 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14211 12442 603 41 0 14170 0 vsize: 56844 [startup+680.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12794 0 0 0 67980 38 0 0 25 0 1 0 545058195 58470400 12509 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14275 12509 603 41 0 14234 0 vsize: 57100 [startup+690.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12868 0 0 0 68980 38 0 0 25 0 1 0 545058195 58736640 12583 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14340 12583 603 41 0 14299 0 vsize: 57360 [startup+700.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 12927 0 0 0 69980 38 0 0 25 0 1 0 545058195 59002880 12642 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14405 12642 603 41 0 14364 0 vsize: 57620 [startup+710.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13008 0 0 0 70980 38 0 0 25 0 1 0 545058195 59412480 12723 4294967295 134512640 134672761 3221224624 3221223760 134565064 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14505 12723 603 41 0 14464 0 vsize: 58020 [startup+720.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13077 0 0 0 71980 39 0 0 25 0 1 0 545058195 59674624 12792 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14569 12792 603 41 0 14528 0 vsize: 58276 [startup+730.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13171 0 0 0 72980 39 0 0 25 0 1 0 545058195 60071936 12886 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14666 12886 603 41 0 14625 0 vsize: 58664 [startup+740.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13251 0 0 0 73980 39 0 0 25 0 1 0 545058195 60338176 12966 4294967295 134512640 134672761 3221224624 3221223728 134560207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14731 12966 603 41 0 14690 0 vsize: 58924 [startup+750.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13315 0 0 0 74980 39 0 0 25 0 1 0 545058195 60596224 13030 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14794 13030 603 41 0 14753 0 vsize: 59176 [startup+760.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13387 0 0 0 75980 40 0 0 25 0 1 0 545058195 60862464 13102 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14859 13102 603 41 0 14818 0 vsize: 59436 [startup+770.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13448 0 0 0 76980 40 0 0 25 0 1 0 545058195 61116416 13163 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14921 13163 603 41 0 14880 0 vsize: 59684 [startup+780.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13532 0 0 0 77980 40 0 0 25 0 1 0 545058195 61517824 13247 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15019 13247 603 41 0 14978 0 vsize: 60076 [startup+790.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13596 0 0 0 78980 40 0 0 25 0 1 0 545058195 61775872 13311 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15082 13311 603 41 0 15041 0 vsize: 60328 [startup+800.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13690 0 0 0 79979 41 0 0 25 0 1 0 545058195 61976576 13384 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13384 603 41 0 15090 0 vsize: 60524 [startup+810.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13690 0 0 0 80980 41 0 0 25 0 1 0 545058195 61976576 13384 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13384 603 41 0 15090 0 vsize: 60524 [startup+820.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13690 0 0 0 81980 41 0 0 25 0 1 0 545058195 61976576 13384 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13384 603 41 0 15090 0 vsize: 60524 [startup+830.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13690 0 0 0 82980 41 0 0 25 0 1 0 545058195 61976576 13384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13384 603 41 0 15090 0 vsize: 60524 [startup+840.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13690 0 0 0 83980 41 0 0 25 0 1 0 545058195 61976576 13384 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13384 603 41 0 15090 0 vsize: 60524 [startup+850.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 84980 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+860.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 85980 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+870.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 86980 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+880.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 87981 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+890.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 88981 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+900.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 89981 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+910.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 90982 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+920.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 91982 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+930.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 92982 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+940.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 93982 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223760 134560613 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+950.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 94982 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+960.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 95983 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+970.137 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 96983 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+980.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 97983 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+990.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 98983 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1000.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 99983 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1010.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 100983 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1020.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 101984 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1030.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 102984 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1040.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 103984 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1050.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 104984 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1060.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 105984 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1070.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 106984 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1080.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 107985 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1090.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 108985 41 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1100.14 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 109984 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1110.14 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 110984 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1120.14 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 111985 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1130.14 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 112985 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1140.14 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 113985 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1150.14 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 114985 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223728 134559838 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1160.14 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 115985 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1170.14 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 116985 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1180.14 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 117985 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1190.14 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 118986 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 [startup+1200.14 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 31434 Raw data (stat): 31434 (minisat+) R 31433 22612 22611 0 -1 0 13691 0 0 0 119986 42 0 0 25 0 1 0 545058195 61976576 13385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15131 13385 603 41 0 15090 0 vsize: 60524 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.17 s] Raw data (loadavg): 1.01 0.99 0.91 1/54 31434 Raw data (stat): 31434 (minisat+) Z 31433 22612 22611 0 -1 12 13694 0 0 0 119986 45 0 0 25 0 1 0 545058195 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.17 CPU time (s): 1200.32 CPU user time (s): 1199.86 CPU system time (s): 0.45593 CPU usage (%): 100.013 Max. virtual memory (Kb): 60524 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####