Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare2.opb |
MD5SUM | 111dddb6adf389a5275ab413feff6076 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 429056 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 210 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 7516192761 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 7516192761 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1201.36 |
Number of variables | 270 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 7 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 90 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc12 THE 2005-04-21 23:20:00 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13533 boxname=wulflinc12 idbench=1041 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 111dddb6adf389a5275ab413feff6076 /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-markshare2.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-markshare2.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-markshare2.opb IDLAUNCH: 13533 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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.091 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: 224656 kB Buffers: 33520 kB Cached: 755044 kB SwapCached: 508 kB Active: 157588 kB Inactive: 633108 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 224404 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5276 kB Slab: 13744 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 23:40:03 (client local time) WITH STATUS 10 IN 1200.21 SECONDS stats: 13533 7 1200.21 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 14 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 12]---> Adder-cost: 354 maxlim: 3452927 bits: 23/22 c ---[ 10]---> Adder-cost: 380 maxlim: 3689471 bits: 23/22 c ---[ 8]---> Adder-cost: 350 maxlim: 3561471 bits: 23/22 c ---[ 6]---> Adder-cost: 340 maxlim: 3823615 bits: 23/22 c ---[ 4]---> Adder-cost: 390 maxlim: 3614719 bits: 23/22 c ---[ 2]---> Adder-cost: 358 maxlim: 3749887 bits: 23/22 c ---[ 0]---> Adder-cost: 374 maxlim: 3556351 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 17222 61228 | 5740 0 0 nan | 0.000 % | c | 100 | 17222 61228 | 6314 100 354 3.5 | 12.727 % | c | 250 | 17214 61202 | 6945 249 1122 4.5 | 12.761 % | c ============================================================================== c [1mFound solution: 7023616[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1069 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 344 | 20137 68094 | 6712 343 1819 5.3 | 12.761 % | c | 444 | 20137 68094 | 7383 443 12460 28.1 | 9.716 % | c | 594 | 20129 68068 | 8121 592 32128 54.3 | 9.742 % | c ============================================================================== c [1mFound solution: 6494208[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 701 | 20179 68196 | 6726 698 39584 56.7 | 9.742 % | c ============================================================================== c [1mFound solution: 6488064[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 765 | 20197 68242 | 6732 762 49821 65.4 | 9.742 % | c ============================================================================== c [1mFound solution: 6160384[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 788 | 20216 68289 | 6738 785 50389 64.2 | 9.742 % | c ============================================================================== c [1mFound solution: 5926912[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 855 | 20240 68347 | 6746 852 61121 71.7 | 9.742 % | c | 957 | 20240 68347 | 7420 954 74178 77.8 | 9.794 % | c | 1108 | 20232 68321 | 8162 1104 93548 84.7 | 9.820 % | c | 1333 | 20232 68321 | 8978 1329 120525 90.7 | 9.820 % | c | 1672 | 20232 68321 | 9876 1668 139880 83.9 | 9.820 % | c ============================================================================== c [1mFound solution: 5922816[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1696 | 20253 68372 | 6751 1692 142492 84.2 | 9.820 % | c ============================================================================== c [1mFound solution: 5918720[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1764 | 20277 68430 | 6759 1760 150818 85.7 | 9.820 % | c | 1865 | 20277 68430 | 7434 1861 160047 86.0 | 9.833 % | c | 2015 | 20277 68430 | 8178 2011 171202 85.1 | 9.833 % | c | 2240 | 20277 68430 | 8996 2236 190935 85.4 | 9.833 % | c ============================================================================== c [1mFound solution: 5232640[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2385 | 20301 68492 | 6767 2381 203817 85.6 | 9.833 % | c | 2485 | 20301 68492 | 7443 2481 212464 85.6 | 9.841 % | c | 2636 | 20301 68492 | 8188 2632 227536 86.4 | 9.841 % | c ============================================================================== c [1mFound solution: 4543488[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2817 | 20332 68567 | 6777 2813 235715 83.8 | 9.841 % | c ============================================================================== c [1mFound solution: 4190208[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2907 | 20341 68592 | 6780 2903 239840 82.6 | 9.841 % | c | 3008 | 20341 68592 | 7458 3004 253054 84.2 | 9.862 % | c | 3160 | 20341 68592 | 8203 3156 264777 83.9 | 9.862 % | c | 3386 | 20333 68566 | 9024 3381 282561 83.6 | 9.887 % | c | 3724 | 20333 68566 | 9926 3719 308609 83.0 | 9.887 % | c | 4230 | 20325 68540 | 10919 4224 359168 85.0 | 9.912 % | c | 4991 | 20317 68514 | 12011 4984 448360 90.0 | 9.937 % | c | 6131 | 20309 68488 | 13212 6123 544455 88.9 | 9.962 % | c | 7840 | 20301 68462 | 14533 7831 756142 96.6 | 9.987 % | c | 10402 | 20269 68358 | 15986 10389 1034854 99.6 | 10.088 % | c | 14246 | 20253 68306 | 17585 14231 1313201 92.3 | 10.138 % | c ============================================================================== c [1mFound solution: 3871744[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17662 | 20280 68371 | 6760 17647 1712464 97.0 | 10.138 % | c | 17762 | 20280 68371 | 7436 4512 392059 86.9 | 10.141 % | c | 17913 | 20280 68371 | 8179 4663 405086 86.9 | 10.141 % | c | 18139 | 20280 68371 | 8997 4889 423670 86.7 | 10.141 % | c | 18477 | 20280 68371 | 9897 5227 454333 86.9 | 10.141 % | c | 18984 | 20280 68371 | 10887 5734 495202 86.4 | 10.141 % | c | 19744 | 20280 68371 | 11975 6494 570493 87.8 | 10.141 % | c | 20884 | 20280 68371 | 13173 7634 623596 81.7 | 10.141 % | c | 22592 | 20266 68327 | 14490 9340 765876 82.0 | 10.191 % | c ============================================================================== c [1mFound solution: 3836928[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24403 | 20295 68396 | 6765 11151 886232 79.5 | 10.191 % | c | 24503 | 20295 68396 | 7441 5676 320244 56.4 | 10.190 % | c | 24654 | 20295 68396 | 8185 5827 331873 57.0 | 10.190 % | c | 24879 | 20295 68396 | 9004 6052 354549 58.6 | 10.190 % | c | 25218 | 20295 68396 | 9904 6391 379680 59.4 | 10.190 % | c | 25724 | 20295 68396 | 10895 6897 398476 57.8 | 10.190 % | c | 26483 | 20295 68396 | 11984 7656 486672 63.6 | 10.190 % | c | 27624 | 20295 68396 | 13183 8797 548152 62.3 | 10.190 % | c | 29333 | 20288 68380 | 14501 10505 700085 66.6 | 10.215 % | c ============================================================================== c [1mFound solution: 3792896[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30965 | 20302 68414 | 6767 12137 892437 73.5 | 10.215 % | c | 31066 | 20302 68414 | 7443 6170 432933 70.2 | 10.228 % | c | 31218 | 20302 68414 | 8188 6322 437963 69.3 | 10.228 % | c | 31444 | 20302 68414 | 9006 6548 459010 70.1 | 10.228 % | c | 31781 | 20302 68414 | 9907 6885 474941 69.0 | 10.228 % | c | 32287 | 20302 68414 | 10898 7391 516443 69.9 | 10.228 % | c | 33046 | 20302 68414 | 11988 8150 564384 69.2 | 10.228 % | c | 34185 | 20302 68414 | 13186 9289 661071 71.2 | 10.228 % | c ============================================================================== c [1mFound solution: 3509248[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35428 | 20307 68419 | 6769 10531 710963 67.5 | 10.228 % | c | 35530 | 20307 68419 | 7445 5368 259347 48.3 | 10.265 % | c | 35682 | 20307 68419 | 8190 5520 269127 48.8 | 10.265 % | c | 35907 | 20307 68419 | 9009 5745 281440 49.0 | 10.265 % | c | 36245 | 20307 68419 | 9910 6083 308126 50.7 | 10.265 % | c | 36751 | 20307 68419 | 10901 6589 333711 50.6 | 10.265 % | c | 37510 | 20307 68419 | 11991 7348 385155 52.4 | 10.265 % | c | 38649 | 20307 68419 | 13190 8487 441397 52.0 | 10.265 % | c | 40359 | 20307 68419 | 14509 10197 558964 54.8 | 10.265 % | c | 42921 | 20307 68419 | 15960 12759 841784 66.0 | 10.265 % | c | 46767 | 20307 68419 | 17557 16605 1186457 71.5 | 10.265 % | c | 52533 | 20307 68419 | 19312 12796 894451 69.9 | 10.265 % | c | 61182 | 20307 68419 | 21244 11191 693224 61.9 | 10.265 % | c | 74157 | 20307 68419 | 23368 13001 715476 55.0 | 10.265 % | c | 93619 | 20307 68419 | 25705 20163 1499595 74.4 | 10.265 % | c ============================================================================== c [1mFound solution: 3228672[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 119436 | 20314 68426 | 6771 18890 1282179 67.9 | 10.265 % | c | 119537 | 20314 68426 | 7448 4824 243711 50.5 | 10.322 % | c | 119688 | 20314 68426 | 8192 4975 248947 50.0 | 10.322 % | c | 119914 | 20314 68426 | 9012 5201 262506 50.5 | 10.322 % | c | 120252 | 20314 68426 | 9913 5539 286002 51.6 | 10.322 % | c | 120760 | 20314 68426 | 10904 6047 307590 50.9 | 10.322 % | c | 121521 | 20314 68426 | 11995 6808 353352 51.9 | 10.322 % | c | 122662 | 20314 68426 | 13194 7949 493941 62.1 | 10.322 % | c | 124371 | 20314 68426 | 14514 9658 639691 66.2 | 10.322 % | c | 126933 | 20314 68426 | 15965 12220 865667 70.8 | 10.322 % | c | 130778 | 20314 68426 | 17562 16065 1113387 69.3 | 10.322 % | c | 136544 | 20307 68411 | 19318 12438 673798 54.2 | 10.371 % | c | 145194 | 20307 68411 | 21250 10739 1086432 101.2 | 10.371 % | c | 158171 | 20299 68389 | 23375 12512 692110 55.3 | 10.421 % | c | 177632 | 20286 68361 | 25712 19588 1743706 89.0 | 10.521 % | c | 206825 | 20286 68361 | 28284 21608 1986898 92.0 | 10.521 % | c | 250615 | 20259 68296 | 31112 17604 1442774 82.0 | 10.671 % | c ============================================================================== c [1mFound solution: 3090432[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 265322 | 20259 68302 | 6753 14118 1121736 79.5 | 10.671 % | c | 265422 | 20259 68302 | 7428 7159 474900 66.3 | 10.804 % | c | 265573 | 20259 68302 | 8171 7310 479753 65.6 | 10.804 % | c | 265801 | 20259 68302 | 8988 7538 483583 64.2 | 10.804 % | c | 266138 | 20259 68302 | 9887 7875 491646 62.4 | 10.804 % | c ============================================================================== c [1mFound solution: 3012608[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 266412 | 20277 68348 | 6759 8149 497096 61.0 | 10.804 % | c | 266512 | 20277 68348 | 7434 4175 128007 30.7 | 10.816 % | c | 266663 | 20277 68348 | 8178 4326 131572 30.4 | 10.816 % | c | 266888 | 20277 68348 | 8996 4551 138163 30.4 | 10.816 % | c | 267229 | 20277 68348 | 9895 4892 143487 29.3 | 10.816 % | c ============================================================================== c [1mFound solution: 2960384[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 267434 | 20291 68382 | 6763 5097 153533 30.1 | 10.816 % | c | 267536 | 20291 68382 | 7439 5199 161846 31.1 | 10.827 % | c | 267686 | 20291 68382 | 8183 5349 170477 31.9 | 10.827 % | c | 267911 | 20282 68355 | 9001 5573 185872 33.4 | 10.877 % | c | 268248 | 20282 68355 | 9901 5910 206816 35.0 | 10.877 % | c | 268757 | 20282 68355 | 10891 6419 230843 36.0 | 10.877 % | c | 269516 | 20282 68355 | 11981 7178 288249 40.2 | 10.877 % | c | 270655 | 20282 68355 | 13179 8317 367200 44.2 | 10.877 % | c ============================================================================== c [1mFound solution: 2712576[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 272032 | 20294 68379 | 6764 9693 444611 45.9 | 10.877 % | c | 272132 | 20294 68379 | 7440 4947 203000 41.0 | 10.932 % | c | 272282 | 20294 68379 | 8184 5097 209884 41.2 | 10.932 % | c | 272509 | 20294 68379 | 9002 5324 216068 40.6 | 10.932 % | c | 272848 | 20294 68379 | 9903 5663 252577 44.6 | 10.932 % | c | 273355 | 20294 68379 | 10893 6170 273314 44.3 | 10.932 % | c | 274115 | 20294 68379 | 11982 6930 354800 51.2 | 10.932 % | c | 275254 | 20294 68379 | 13181 8069 427580 53.0 | 10.932 % | c ============================================================================== c [1mFound solution: 2147328[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 275572 | 20305 68408 | 6768 8387 431860 51.5 | 10.932 % | c | 275672 | 20305 68408 | 7444 4294 182758 42.6 | 10.949 % | c | 275823 | 20305 68408 | 8189 4445 202925 45.7 | 10.949 % | c | 276049 | 20305 68408 | 9008 4671 216826 46.4 | 10.949 % | c | 276388 | 20305 68408 | 9909 5010 225188 44.9 | 10.949 % | c | 276894 | 20305 68408 | 10899 5516 247985 45.0 | 10.949 % | c | 277655 | 20305 68408 | 11989 6277 305413 48.7 | 10.949 % | c | 278794 | 20305 68408 | 13188 7416 357800 48.2 | 10.949 % | c | 280502 | 20305 68408 | 14507 9124 461871 50.6 | 10.949 % | c | 283065 | 20305 68408 | 15958 11687 710315 60.8 | 10.949 % | c | 286909 | 20305 68408 | 17554 15531 911059 58.7 | 10.949 % | c | 292676 | 20292 68378 | 19309 11981 580839 48.5 | 11.048 % | c | 301325 | 20292 68378 | 21240 10402 676281 65.0 | 11.048 % | c | 314300 | 20292 68378 | 23364 12071 790578 65.5 | 11.048 % | c | 333763 | 20273 68335 | 25701 19251 1138815 59.2 | 11.196 % | c | 362955 | 20259 68295 | 28271 20901 970705 46.4 | 11.271 % | c | 406746 | 20259 68295 | 31098 19932 977282 49.0 | 11.271 % | c | 472430 | 20230 68231 | 34208 29183 1453573 49.8 | 11.469 % | #### 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.84 0.94 0.91 2/54 7995 Raw data (stat): 7995 (runsolver) R 7994 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490765985 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0007 s] Raw data (loadavg): 0.87 0.94 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 1311 0 0 0 995 4 0 0 25 0 1 0 490765985 6991872 1289 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1707 1289 603 41 0 1666 0 vsize: 6828 [startup+20.0019 s] Raw data (loadavg): 0.89 0.94 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 1731 0 0 0 1993 5 0 0 25 0 1 0 490765985 8716288 1709 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2128 1709 603 41 0 2087 0 vsize: 8512 [startup+30.0028 s] Raw data (loadavg): 0.90 0.94 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2122 0 0 0 2992 7 0 0 25 0 1 0 490765985 10317824 2100 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2519 2100 603 41 0 2478 0 vsize: 10076 [startup+40.0021 s] Raw data (loadavg): 0.92 0.94 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2472 0 0 0 3990 9 0 0 25 0 1 0 490765985 11644928 2450 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2843 2450 603 41 0 2802 0 vsize: 11372 [startup+50.0034 s] Raw data (loadavg): 0.93 0.94 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 4990 9 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2665 603 41 0 3048 0 vsize: 12356 [startup+60.0043 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 5990 9 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134561394 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2665 603 41 0 3048 0 vsize: 12356 [startup+70.0047 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 6989 10 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2665 603 41 0 3048 0 vsize: 12356 [startup+80.0063 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 7989 10 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2665 603 41 0 3048 0 vsize: 12356 [startup+90.0068 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 8989 10 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2665 603 41 0 3048 0 vsize: 12356 [startup+100.007 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 9989 11 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2665 603 41 0 3048 0 vsize: 12356 [startup+110.008 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2687 0 0 0 10989 11 0 0 25 0 1 0 490765985 12652544 2665 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2665 603 41 0 3048 0 vsize: 12356 [startup+120.01 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2688 0 0 0 11988 12 0 0 25 0 1 0 490765985 12652544 2666 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2666 603 41 0 3048 0 vsize: 12356 [startup+130.011 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2688 0 0 0 12988 12 0 0 25 0 1 0 490765985 12652544 2666 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2666 603 41 0 3048 0 vsize: 12356 [startup+140.011 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2690 0 0 0 13988 12 0 0 25 0 1 0 490765985 12652544 2668 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2668 603 41 0 3048 0 vsize: 12356 [startup+150.013 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2690 0 0 0 14987 13 0 0 25 0 1 0 490765985 12652544 2668 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2668 603 41 0 3048 0 vsize: 12356 [startup+160.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2691 0 0 0 15987 13 0 0 25 0 1 0 490765985 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2669 603 41 0 3048 0 vsize: 12356 [startup+170.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2691 0 0 0 16987 13 0 0 25 0 1 0 490765985 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2669 603 41 0 3048 0 vsize: 12356 [startup+180.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2691 0 0 0 17987 14 0 0 25 0 1 0 490765985 12652544 2669 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3089 2669 603 41 0 3048 0 vsize: 12356 [startup+190.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2843 0 0 0 18986 15 0 0 25 0 1 0 490765985 13324288 2821 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3253 2821 603 41 0 3212 0 vsize: 13012 [startup+200.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2911 0 0 0 19986 15 0 0 25 0 1 0 490765985 13594624 2889 4294967295 134512640 134672761 3221224528 3221223664 134560622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3319 2889 603 41 0 3278 0 vsize: 13276 [startup+210.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 2913 0 0 0 20986 15 0 0 25 0 1 0 490765985 13594624 2891 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3319 2891 603 41 0 3278 0 vsize: 13276 [startup+220.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3096 0 0 0 21986 16 0 0 25 0 1 0 490765985 14266368 3074 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3483 3074 603 41 0 3442 0 vsize: 13932 [startup+230.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3365 0 0 0 22984 18 0 0 25 0 1 0 490765985 15331328 3343 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3743 3343 603 41 0 3702 0 vsize: 14972 [startup+240.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3365 0 0 0 23983 18 0 0 25 0 1 0 490765985 15331328 3343 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3743 3343 603 41 0 3702 0 vsize: 14972 [startup+250.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3365 0 0 0 24983 19 0 0 25 0 1 0 490765985 15331328 3343 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3743 3343 603 41 0 3702 0 vsize: 14972 [startup+260.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3372 0 0 0 25983 19 0 0 25 0 1 0 490765985 15474688 3350 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3778 3350 603 41 0 3737 0 vsize: 15112 [startup+270.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3380 0 0 0 26983 19 0 0 25 0 1 0 490765985 15474688 3358 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3778 3358 603 41 0 3737 0 vsize: 15112 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 27982 19 0 0 25 0 1 0 490765985 15609856 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3811 3379 603 41 0 3770 0 vsize: 15244 [startup+290.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 28982 20 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 29982 20 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 30982 20 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+320.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 31982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+330.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 32982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+340.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 33982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+350.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 34982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+360.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 35982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+370.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 36982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+380.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 37982 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+390.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 38983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+400.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 39983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+410.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 40983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+420.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 41983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223484 1075349891 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+430.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3401 0 0 0 42983 21 0 0 25 0 1 0 490765985 15605760 3379 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3810 3379 603 41 0 3769 0 vsize: 15240 [startup+440.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3494 0 0 0 43983 21 0 0 25 0 1 0 490765985 15867904 3472 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3874 3472 603 41 0 3833 0 vsize: 15496 [startup+450.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 3789 0 0 0 44983 22 0 0 25 0 1 0 490765985 17199104 3767 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4199 3767 603 41 0 4158 0 vsize: 16796 [startup+460.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4066 0 0 0 45983 22 0 0 25 0 1 0 490765985 18264064 4044 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4459 4044 603 41 0 4418 0 vsize: 17836 [startup+470.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4128 0 0 0 46982 23 0 0 25 0 1 0 490765985 18530304 4106 4294967295 134512640 134672761 3221224528 3221223664 134565098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4524 4106 603 41 0 4483 0 vsize: 18096 [startup+480.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4128 0 0 0 47982 23 0 0 25 0 1 0 490765985 18530304 4106 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4524 4106 603 41 0 4483 0 vsize: 18096 [startup+490.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4130 0 0 0 48982 23 0 0 25 0 1 0 490765985 18530304 4108 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4524 4108 603 41 0 4483 0 vsize: 18096 [startup+500.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4142 0 0 0 49983 23 0 0 25 0 1 0 490765985 18669568 4120 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4558 4120 603 41 0 4517 0 vsize: 18232 [startup+510.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4244 0 0 0 50983 23 0 0 25 0 1 0 490765985 19066880 4222 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4655 4222 603 41 0 4614 0 vsize: 18620 [startup+520.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4301 0 0 0 51983 23 0 0 25 0 1 0 490765985 19197952 4279 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4279 603 41 0 4646 0 vsize: 18748 [startup+530.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4301 0 0 0 52983 23 0 0 25 0 1 0 490765985 19197952 4279 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4279 603 41 0 4646 0 vsize: 18748 [startup+540.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4301 0 0 0 53983 23 0 0 25 0 1 0 490765985 19197952 4279 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4279 603 41 0 4646 0 vsize: 18748 [startup+550.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4301 0 0 0 54983 23 0 0 25 0 1 0 490765985 19197952 4279 4294967295 134512640 134672761 3221224528 3221223600 134565153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4279 603 41 0 4646 0 vsize: 18748 [startup+560.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 55983 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+570.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 56984 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+580.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 57985 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+590.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 58985 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+600.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 59986 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+610.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 60986 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+620.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 61986 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+630.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 62986 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+640.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 63986 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134561027 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+650.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 64987 23 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+660.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 65985 24 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+670.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 66985 24 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+680.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 67985 24 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223712 134559538 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+690.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4304 0 0 0 68985 24 0 0 25 0 1 0 490765985 19197952 4282 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4687 4282 603 41 0 4646 0 vsize: 18748 [startup+700.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 69985 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223828 134556653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 70986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+720.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 71986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+730.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 72986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+740.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 73986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+750.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 74986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+760.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 75986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+770.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 76986 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 77987 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+790.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 78987 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+800.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 79987 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+810.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 80987 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+820.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 81988 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+830.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 82988 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+840.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 83988 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+850.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 84988 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+860.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 85988 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+870.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 86988 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+880.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 87989 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+890.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 88989 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+900.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 89989 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+910.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 90990 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+920.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 91990 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+930.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 92990 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+940.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 93990 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+950.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 94991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+960.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 95991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+970.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 96991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+980.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 97991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561018 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+990.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 98991 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 99992 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 100992 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 101992 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 102992 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 103992 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 104993 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4478 0 0 0 105993 24 0 0 25 0 1 0 490765985 19996672 4456 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4882 4456 603 41 0 4841 0 vsize: 19528 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 106993 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223664 134560647 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 107993 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 108993 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 109993 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 110994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 111994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 112994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 113994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 114994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 115995 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223664 134560598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 116995 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4513 0 0 0 117994 24 0 0 25 0 1 0 490765985 20258816 4491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4946 4491 603 41 0 4905 0 vsize: 19784 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4687 0 0 0 118994 25 0 0 25 0 1 0 490765985 20926464 4665 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5109 4665 603 41 0 5068 0 vsize: 20436 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 7995 Raw data (stat): 7995 (minisat+) R 7994 25285 25284 0 -1 0 4687 0 0 0 119994 25 0 0 25 0 1 0 490765985 20926464 4665 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5109 4665 603 41 0 5068 0 vsize: 20436 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 7995 Raw data (stat): 7995 (minisat+) Z 7994 25285 25284 0 -1 12 4690 0 0 0 119994 26 0 0 25 0 1 0 490765985 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.09 CPU time (s): 1200.21 CPU user time (s): 1199.94 CPU system time (s): 0.264959 CPU usage (%): 100.01 Max. virtual memory (Kb): 20436 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####