Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare1.opb |
MD5SUM | 6f06e375914e0285ec75de90ad627758 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3712 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 120 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 6291450 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 6291450 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.1 |
Number of variables | 170 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 70 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc8 THE 2005-04-21 16:11:02 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17633 boxname=wulflinc8 idbench=1357 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 6f06e375914e0285ec75de90ad627758 /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-markshare1.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-markshare1.opb IDLAUNCH: 17633 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 874024 kB Buffers: 3788 kB Cached: 135000 kB SwapCached: 0 kB Active: 12580 kB Inactive: 129084 kB HighTotal: 131008 kB HighFree: 56420 kB LowTotal: 903652 kB LowFree: 817604 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6952 kB Slab: 13284 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 16:31:05 (client local time) WITH STATUS 10 IN 1200.18 SECONDS stats: 17633 7 1200.18 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 12 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 10]---> Adder-cost: 304 maxlim: 405119 bits: 20/19 c ---[ 8]---> Adder-cost: 314 maxlim: 431743 bits: 20/19 c ---[ 6]---> Adder-cost: 348 maxlim: 435327 bits: 20/19 c ---[ 4]---> Adder-cost: 318 maxlim: 411775 bits: 20/19 c ---[ 2]---> Adder-cost: 312 maxlim: 410751 bits: 20/19 c ---[ 0]---> Adder-cost: 314 maxlim: 411135 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 12820 45524 | 4273 0 0 nan | 0.000 % | c | 100 | 12820 45524 | 4700 100 583 5.8 | 11.212 % | c ============================================================================== c [1mFound solution: 511232[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 855 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 | 115 | 14928 50449 | 4976 115 713 6.2 | 11.212 % | c | 218 | 14920 50423 | 5473 217 7283 33.6 | 8.450 % | c | 368 | 14920 50423 | 6020 367 18769 51.1 | 8.450 % | c | 593 | 14920 50423 | 6623 592 36809 62.2 | 8.450 % | c | 930 | 14912 50397 | 7285 928 58825 63.4 | 8.484 % | c ============================================================================== c [1mFound solution: 508160[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 | 1311 | 14927 50468 | 4975 1309 91930 70.2 | 8.484 % | c | 1414 | 14927 50468 | 5472 1412 98927 70.1 | 8.489 % | c | 1567 | 14919 50442 | 6019 1564 113420 72.5 | 8.523 % | c | 1794 | 14919 50442 | 6621 1791 129324 72.2 | 8.523 % | c ============================================================================== c [1mFound solution: 481280[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 | 1899 | 14937 50494 | 4979 1896 134567 71.0 | 8.523 % | c | 1999 | 14937 50494 | 5476 1996 140754 70.5 | 8.519 % | c | 2149 | 14937 50494 | 6024 2146 148833 69.4 | 8.519 % | c | 2374 | 14937 50494 | 6627 2371 164400 69.3 | 8.519 % | c ============================================================================== c [1mFound solution: 435072[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 | 2433 | 14949 50522 | 4983 2430 167546 68.9 | 8.519 % | c | 2534 | 14949 50522 | 5481 2531 177093 70.0 | 8.533 % | c | 2685 | 14941 50496 | 6029 2681 186556 69.6 | 8.567 % | c | 2911 | 14941 50496 | 6632 2907 203514 70.0 | 8.567 % | c | 3249 | 14941 50496 | 7295 3245 244508 75.3 | 8.567 % | c | 3755 | 14941 50496 | 8025 3751 292255 77.9 | 8.567 % | c | 4514 | 14941 50496 | 8827 4510 341575 75.7 | 8.567 % | c | 5654 | 14941 50496 | 9710 5650 468535 82.9 | 8.567 % | c | 7362 | 14933 50470 | 10681 7357 615477 83.7 | 8.600 % | c | 9925 | 14925 50444 | 11749 9919 841229 84.8 | 8.634 % | c ============================================================================== c [1mFound solution: 430720[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 | 10164 | 14939 50476 | 4979 10158 857755 84.4 | 8.634 % | c | 10264 | 14939 50476 | 5476 5179 384424 74.2 | 8.644 % | c | 10414 | 14939 50476 | 6024 5329 396662 74.4 | 8.644 % | c | 10639 | 14939 50476 | 6627 5554 417897 75.2 | 8.644 % | c | 10977 | 14939 50476 | 7289 5892 445678 75.6 | 8.644 % | c | 11483 | 14939 50476 | 8018 6398 493666 77.2 | 8.644 % | c | 12242 | 14939 50476 | 8820 7157 567456 79.3 | 8.644 % | c | 13381 | 14939 50476 | 9702 8296 676789 81.6 | 8.644 % | c ============================================================================== c [1mFound solution: 424576[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 | 14095 | 14945 50493 | 4981 9010 744526 82.6 | 8.644 % | c | 14195 | 14945 50493 | 5479 4605 343883 74.7 | 8.669 % | c | 14346 | 14945 50493 | 6027 4756 352759 74.2 | 8.669 % | c | 14571 | 14945 50493 | 6629 4981 365164 73.3 | 8.669 % | c | 14909 | 14945 50493 | 7292 5319 391290 73.6 | 8.669 % | c ============================================================================== c [1mFound solution: 401408[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 | 15041 | 14955 50515 | 4985 5451 404775 74.3 | 8.669 % | c | 15142 | 14955 50515 | 5483 2827 161070 57.0 | 8.691 % | c | 15293 | 14955 50515 | 6031 2978 169426 56.9 | 8.691 % | c | 15519 | 14955 50515 | 6635 3204 190669 59.5 | 8.691 % | c | 15856 | 14955 50515 | 7298 3541 210095 59.3 | 8.691 % | c | 16364 | 14949 50497 | 8028 4048 257813 63.7 | 8.725 % | c | 17124 | 14949 50497 | 8831 4808 319608 66.5 | 8.725 % | c | 18263 | 14949 50497 | 9714 5947 408827 68.7 | 8.725 % | c | 19973 | 14949 50497 | 10685 7657 514369 67.2 | 8.725 % | c | 22535 | 14949 50497 | 11754 10219 725324 71.0 | 8.725 % | c | 26379 | 14941 50471 | 12929 7738 611167 79.0 | 8.758 % | c ============================================================================== c [1mFound solution: 396032[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 | 27088 | 14953 50499 | 4984 8447 701896 83.1 | 8.758 % | c | 27189 | 14953 50499 | 5482 4325 322480 74.6 | 8.777 % | c | 27340 | 14953 50499 | 6030 4476 334565 74.7 | 8.777 % | c | 27566 | 14953 50499 | 6633 4702 352775 75.0 | 8.777 % | c | 27904 | 14953 50499 | 7297 5040 379892 75.4 | 8.777 % | c | 28410 | 14953 50499 | 8026 5546 421562 76.0 | 8.777 % | c | 29169 | 14953 50499 | 8829 6305 474041 75.2 | 8.777 % | c | 30309 | 14953 50499 | 9712 7445 580343 78.0 | 8.777 % | c | 32018 | 14947 50486 | 10683 9153 744520 81.3 | 8.844 % | c | 34580 | 14947 50486 | 11752 5864 429656 73.3 | 8.844 % | c | 38424 | 14939 50460 | 12927 9707 719681 74.1 | 8.878 % | c | 44191 | 14917 50390 | 14219 8519 572810 67.2 | 8.978 % | c ============================================================================== c [1mFound solution: 389248[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 | 47913 | 14929 50422 | 4976 12241 889985 72.7 | 8.978 % | c | 48015 | 14929 50422 | 5473 3163 161261 51.0 | 8.991 % | c | 48166 | 14929 50422 | 6020 3314 174071 52.5 | 8.991 % | c | 48392 | 14929 50422 | 6623 3540 195446 55.2 | 8.991 % | c | 48730 | 14929 50422 | 7285 3878 223677 57.7 | 8.991 % | c | 49237 | 14929 50422 | 8013 4385 278053 63.4 | 8.991 % | c | 49998 | 14929 50422 | 8815 5146 360261 70.0 | 8.991 % | c | 51138 | 14929 50422 | 9696 6286 457548 72.8 | 8.991 % | c | 52847 | 14929 50422 | 10666 7995 595650 74.5 | 8.991 % | c | 55410 | 14929 50422 | 11733 10558 774167 73.3 | 8.991 % | c ============================================================================== c [1mFound solution: 377728[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 | 56352 | 14920 50389 | 4973 11498 829497 72.1 | 8.991 % | c | 56453 | 14920 50389 | 5470 2976 126077 42.4 | 9.076 % | c | 56603 | 14920 50389 | 6017 3126 135668 43.4 | 9.076 % | c | 56829 | 14920 50389 | 6619 3352 154566 46.1 | 9.076 % | c | 57167 | 14920 50389 | 7280 3690 180132 48.8 | 9.076 % | c | 57674 | 14920 50389 | 8009 4197 208039 49.6 | 9.076 % | c | 58435 | 14920 50389 | 8809 4958 280274 56.5 | 9.076 % | c | 59576 | 14920 50389 | 9690 6099 363954 59.7 | 9.076 % | c | 61285 | 14920 50389 | 10660 7808 488158 62.5 | 9.076 % | c | 63848 | 14920 50389 | 11726 10371 708658 68.3 | 9.076 % | c | 67693 | 14920 50389 | 12898 7831 507587 64.8 | 9.076 % | c ============================================================================== c [1mFound solution: 306944[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 | 72031 | 14923 50389 | 4974 12168 780818 64.2 | 9.076 % | c | 72132 | 14923 50389 | 5471 3143 114668 36.5 | 9.124 % | c | 72283 | 14923 50389 | 6018 3294 126047 38.3 | 9.124 % | c | 72509 | 14923 50389 | 6620 3520 134740 38.3 | 9.124 % | c | 72846 | 14923 50389 | 7282 3857 148492 38.5 | 9.124 % | c | 73353 | 14923 50389 | 8010 4364 174667 40.0 | 9.124 % | c ============================================================================== c [1mFound solution: 282624[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 | 74024 | 14934 50414 | 4978 5035 211786 42.1 | 9.124 % | c | 74125 | 14934 50414 | 5475 5136 215318 41.9 | 9.139 % | c | 74275 | 14934 50414 | 6023 5286 219636 41.6 | 9.139 % | c | 74502 | 14934 50414 | 6625 5513 225641 40.9 | 9.139 % | c | 74840 | 14934 50414 | 7288 5851 247004 42.2 | 9.139 % | c | 75348 | 14934 50414 | 8017 6359 269180 42.3 | 9.139 % | c | 76107 | 14934 50414 | 8818 7118 317253 44.6 | 9.139 % | c | 77246 | 14934 50414 | 9700 8257 408361 49.5 | 9.139 % | c ============================================================================== c [1mFound solution: 280960[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 | 77625 | 14944 50437 | 4981 8636 434637 50.3 | 9.139 % | c | 77725 | 14944 50437 | 5479 4418 204354 46.3 | 9.157 % | c | 77876 | 14944 50437 | 6027 4569 209208 45.8 | 9.157 % | c | 78105 | 14944 50437 | 6629 4798 214379 44.7 | 9.157 % | c | 78442 | 14944 50437 | 7292 5135 229599 44.7 | 9.157 % | c | 78948 | 14944 50437 | 8021 5641 259177 45.9 | 9.157 % | c | 79708 | 14944 50437 | 8824 6401 306245 47.8 | 9.157 % | c | 80847 | 14944 50437 | 9706 7540 367966 48.8 | 9.157 % | c | 82555 | 14944 50437 | 10677 9248 448135 48.5 | 9.157 % | c | 85117 | 14944 50437 | 11744 6099 224259 36.8 | 9.157 % | c | 88961 | 14944 50437 | 12919 9943 423222 42.6 | 9.157 % | c | 94727 | 14944 50437 | 14211 8805 393689 44.7 | 9.157 % | c ============================================================================== c [1mFound solution: 276864[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 | 95408 | 14951 50454 | 4983 9486 452297 47.7 | 9.157 % | c | 95508 | 14951 50454 | 5481 4843 225668 46.6 | 9.181 % | c | 95660 | 14951 50454 | 6029 4995 228247 45.7 | 9.181 % | c | 95886 | 14951 50454 | 6632 5221 235950 45.2 | 9.181 % | c | 96224 | 14951 50454 | 7295 5559 268280 48.3 | 9.181 % | c | 96732 | 14951 50454 | 8025 6067 288367 47.5 | 9.181 % | c | 97491 | 14951 50454 | 8827 6826 312807 45.8 | 9.181 % | c ============================================================================== c [1mFound solution: 270976[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 | 98233 | 14960 50474 | 4986 7568 367612 48.6 | 9.181 % | c | 98337 | 14960 50474 | 5484 3888 149120 38.4 | 9.202 % | c | 98487 | 14960 50474 | 6033 4038 153879 38.1 | 9.202 % | c | 98712 | 14960 50474 | 6636 4263 159883 37.5 | 9.202 % | c | 99049 | 14960 50474 | 7300 4600 183162 39.8 | 9.202 % | c | 99556 | 14960 50474 | 8030 5107 209351 41.0 | 9.202 % | c | 100316 | 14960 50474 | 8833 5867 237677 40.5 | 9.202 % | c | 101455 | 14960 50474 | 9716 7006 288228 41.1 | 9.202 % | c | 103163 | 14960 50474 | 10687 8714 351450 40.3 | 9.202 % | c | 105728 | 14960 50474 | 11756 11279 479582 42.5 | 9.202 % | c | 109572 | 14960 50474 | 12932 8939 396000 44.3 | 9.202 % | c | 115338 | 14960 50474 | 14225 7801 349348 44.8 | 9.202 % | c | 123987 | 14960 50474 | 15648 8933 343695 38.5 | 9.202 % | c ============================================================================== c [1mFound solution: 254080[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 | 131533 | 14968 50495 | 4989 16479 780422 47.4 | 9.202 % | c | 131634 | 14968 50495 | 5487 4221 168757 40.0 | 9.220 % | c | 131784 | 14968 50495 | 6036 4371 169898 38.9 | 9.220 % | c | 132010 | 14968 50495 | 6640 4597 176589 38.4 | 9.220 % | c | 132347 | 14968 50495 | 7304 4934 189055 38.3 | 9.220 % | c | 132853 | 14968 50495 | 8034 5440 207752 38.2 | 9.220 % | c | 133613 | 14968 50495 | 8838 6200 227931 36.8 | 9.220 % | c | 134753 | 14968 50495 | 9722 7340 283754 38.7 | 9.220 % | c | 136462 | 14968 50495 | 10694 9049 447766 49.5 | 9.220 % | c | 139024 | 14968 50495 | 11763 11611 572585 49.3 | 9.220 % | c | 142869 | 14968 50495 | 12940 9385 443339 47.2 | 9.220 % | c | 148635 | 14968 50495 | 14234 8359 334862 40.1 | 9.220 % | c | 157284 | 14968 50495 | 15657 9559 389308 40.7 | 9.220 % | c | 170258 | 14968 50495 | 17223 14357 698508 48.7 | 9.220 % | c | 189721 | 14968 50495 | 18945 15791 813245 51.5 | 9.220 % | c ============================================================================== c [1mFound solution: 235264[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 | 209972 | 14970 50498 | 4990 16339 752560 46.1 | 9.220 % | c | 210072 | 14970 50498 | 5489 4185 160957 38.5 | 9.301 % | c | 210223 | 14970 50498 | 6037 4336 168165 38.8 | 9.301 % | c | 210448 | 14970 50498 | 6641 4561 175463 38.5 | 9.301 % | c | 210786 | 14970 50498 | 7305 4899 180956 36.9 | 9.301 % | c | 211292 | 14970 50498 | 8036 5405 191541 35.4 | 9.301 % | c | 212051 | 14970 50498 | 8840 6164 213220 34.6 | 9.301 % | c | 213190 | 14962 50480 | 9724 7300 275218 37.7 | 9.367 % | c | 214901 | 14962 50480 | 10696 9011 369149 41.0 | 9.367 % | c | 217464 | 14962 50480 | 11766 11574 526142 45.5 | 9.367 % | c ============================================================================== c [1mFound solution: 212736[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 | 220832 | 14972 50503 | 4990 8677 442359 51.0 | 9.367 % | c | 220932 | 14972 50503 | 5489 4439 192659 43.4 | 9.381 % | c | 221082 | 14972 50503 | 6037 4589 200285 43.6 | 9.381 % | c | 221309 | 14972 50503 | 6641 4816 206834 42.9 | 9.381 % | c | 221648 | 14972 50503 | 7305 5155 218113 42.3 | 9.381 % | c | 222155 | 14963 50484 | 8036 5660 230180 40.7 | 9.480 % | c | 222915 | 14963 50484 | 8840 6420 265964 41.4 | 9.480 % | c | 224054 | 14963 50484 | 9724 7559 305271 40.4 | 9.480 % | c | 225762 | 14963 50484 | 10696 9267 361057 39.0 | 9.480 % | c | 228325 | 14963 50484 | 11766 6101 188143 30.8 | 9.480 % | c | 232172 | 14963 50484 | 12942 9948 383964 38.6 | 9.480 % | c ============================================================================== c [1mFound solution: 154752[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 | 236058 | 14972 50507 | 4990 7150 228313 31.9 | 9.480 % | c | 236160 | 14972 50507 | 5489 3677 92931 25.3 | 9.497 % | c | 236311 | 14972 50507 | 6037 3828 100768 26.3 | 9.497 % | c | 236537 | 14972 50507 | 6641 4054 109068 26.9 | 9.497 % | c | 236874 | 14972 50507 | 7305 4391 119615 27.2 | 9.497 % | c | 237380 | 14972 50507 | 8036 4897 138079 28.2 | 9.497 % | c | 238140 | 14972 50507 | 8840 5657 159058 28.1 | 9.498 % | c | 239280 | 14972 50507 | 9724 6797 192745 28.4 | 9.497 % | c | 240991 | 14972 50507 | 10696 8508 277679 32.6 | 9.497 % | c | 243553 | 14972 50507 | 11766 11070 376719 34.0 | 9.497 % | c | 247397 | 14972 50507 | 12942 8658 405878 46.9 | 9.497 % | c | 253164 | 14972 50507 | 14237 7523 301861 40.1 | 9.497 % | c | 261814 | 14972 50507 | 15660 8724 389636 44.7 | 9.497 % | c | 274788 | 14972 50507 | 17226 13516 547618 40.5 | 9.497 % | c | 294251 | 14964 50485 | 18949 14913 697316 46.8 | 9.563 % | c | 323444 | 14948 50449 | 20844 14609 643927 44.1 | 9.727 % | c | 367234 | 14929 50406 | 22928 15159 664222 43.8 | 9.924 % | c | 432918 | 14919 50384 | 25221 21945 980206 44.7 | 10.023 % | c | 531444 | 14914 50373 | 27743 16971 739734 43.6 | 10.089 % | c ============================================================================== c [1mFound solution: 147072[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 | 551980 | 14919 50385 | 4973 22813 921144 40.4 | 10.089 % | c | 552080 | 14919 50385 | 5470 2952 67935 23.0 | 10.174 % | c | 552231 | 14919 50385 | 6017 3103 69955 22.5 | 10.174 % | c | 552457 | 14919 50385 | 6619 3329 85586 25.7 | 10.174 % | c | 552796 | 14919 50385 | 7280 3668 100834 27.5 | 10.174 % | c | 553304 | 14919 50385 | 8009 4176 118179 28.3 | 10.174 % | c | 554063 | 14919 50385 | 8809 4935 154288 31.3 | 10.174 % | c | 555203 | 14919 50385 | 9690 6075 205886 33.9 | 10.174 % | c | 556915 | 14919 50385 | 10660 7787 287187 36.9 | 10.174 % | c | 559478 | 14919 50385 | 11726 10350 387740 37.5 | 10.174 % | c | 563322 | 14919 50385 | 12898 7968 290882 36.5 | 10.174 % | c | 569088 | 14919 50385 | 14188 6967 262229 37.6 | 10.174 % | c | 577739 | 14919 50385 | 15607 8244 334493 40.6 | 10.174 % | c | 590714 | 14919 50385 | 17168 13102 586851 44.8 | 10.174 % | c ============================================================================== c [1mFound solution: 141440[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 | 591860 | 14931 50412 | 4977 14248 635435 44.6 | 10.174 % | c | 591963 | 14931 50412 | 5474 3665 110627 30.2 | 10.187 % | c | 592113 | 14931 50412 | 6022 3815 113648 29.8 | 10.187 % | c | 592338 | 14931 50412 | 6624 4040 124359 30.8 | 10.187 % | c | 592676 | 14931 50412 | 7286 4378 135745 31.0 | 10.187 % | c | 593185 | 14931 50412 | 8015 4887 154926 31.7 | 10.187 % | c ============================================================================== c [1mFound solution: 127360[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 593687 | 14892 50276 | 4964 5383 187551 34.8 | 10.187 % | c | 593787 | 14892 50276 | 5460 2792 79830 28.6 | 10.402 % | c | 593937 | 14892 50276 | 6006 2942 82515 28.0 | 10.402 % | c | 594162 | 14892 50276 | 6607 3167 90802 28.7 | 10.402 % | c | 594499 | 14892 50276 | 7267 3504 102574 29.3 | 10.402 % | c | 595005 | 14892 50276 | 7994 4010 121322 30.3 | 10.402 % | c | 595765 | 14892 50276 | 8794 4770 157152 32.9 | 10.402 % | c | 596904 | 14892 50276 | 9673 5909 201729 34.1 | 10.402 % | c | 598613 | 14892 50276 | 10640 7618 290927 38.2 | 10.402 % | c | 601175 | 14892 50276 | 11704 10180 403974 39.7 | 10.402 % | c | 605019 | 14851 50183 | 12875 7787 288315 37.0 | 10.795 % | c | 610786 | 14851 50183 | 14162 13554 589955 43.5 | 10.795 % | c | 619435 | 14829 50132 | 15579 14797 637237 43.1 | 11.057 % | c | 632410 | 14829 50132 | 17137 11330 497016 43.9 | 11.057 % | c | 651871 | 14829 50132 | 18850 12828 544496 42.4 | 11.057 % | c | 681063 | 14818 50106 | 20735 12477 417985 33.5 | 11.187 % | c | 724852 | 14797 50058 | 22809 13453 508999 37.8 | 11.416 % | c ============================================================================== c [1mFound solution: 117632[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 725185 | 14804 50076 | 4934 13786 517662 37.5 | 11.416 % | c | 725287 | 14804 50076 | 5427 3549 91459 25.8 | 11.430 % | c | 725438 | 14804 50076 | 5970 3700 96454 26.1 | 11.430 % | c | 725663 | 14804 50076 | 6567 3925 103115 26.3 | 11.430 % | c | 726000 | 14804 50076 | 7223 4262 109958 25.8 | 11.430 % | c | 726506 | 14804 50076 | 7946 4768 126560 26.5 | 11.430 % | c | 727266 | 14804 50076 | 8740 5528 156340 28.3 | 11.430 % | c | 728405 | 14804 50076 | 9614 6667 194011 29.1 | 11.430 % | c | 730114 | 14804 50076 | 10576 8376 265522 31.7 | 11.430 % | c | 732676 | 14804 50076 | 11634 10938 367817 33.6 | 11.430 % | c | 736521 | 14804 50076 | 12797 8592 319410 37.2 | 11.430 % | c ============================================================================== c [1mFound solution: 113536[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 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 738861 | 14810 50092 | 4936 10932 465586 42.6 | 11.430 % | c | 738961 | 14810 50092 | 5429 2833 99866 35.3 | 11.444 % | c | 739112 | 14810 50092 | 5972 2984 102707 34.4 | 11.444 % | c | 739339 | 14810 50092 | 6569 3211 107372 33.4 | 11.444 % | c | 739677 | 14810 50092 | 7226 3549 115876 32.7 | 11.444 % | c | 740183 | 14810 50092 | 7949 4055 128536 31.7 | 11.444 % | c | 740943 | 14810 50092 | 8744 4815 150532 31.3 | 11.444 % | c | 742083 | 14810 50092 | 9618 5955 182592 30.7 | 11.444 % | c | 743791 | 14810 50092 | 10580 7663 261883 34.2 | 11.444 % | c | 746355 | 14810 50092 | 11638 10227 355624 34.8 | 11.444 % | c | 750199 | 14810 50092 | 12802 7898 256703 32.5 | 11.444 % | c | 755965 | 14810 50092 | 14082 6952 251331 36.2 | 11.444 % | c | 764615 | 14810 50092 | 15491 8135 295700 36.3 | 11.444 % | c | 777590 | 14810 50092 | 17040 12960 564926 43.6 | 11.444 % | c | 797051 | 14810 50092 | 18744 14662 547954 37.4 | 11.444 % | c | 826243 | 14790 50045 | 20618 14787 532928 36.0 | 11.705 % | c | 870032 | 14790 50045 | 22680 15957 753152 47.2 | 11.705 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.98 0.93 2/54 722 Raw data (stat): 722 (runsolver) R 721 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 474630561 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0003 s] Raw data (loadavg): 0.93 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1247 0 0 0 996 2 0 0 25 0 1 0 474630561 6582272 1225 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1607 1225 603 41 0 1566 0 vsize: 6428 [startup+19.9999 s] Raw data (loadavg): 0.94 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1634 0 0 0 1994 4 0 0 25 0 1 0 474630561 8183808 1612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1998 1612 603 41 0 1957 0 vsize: 7992 [startup+30.0007 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1634 0 0 0 2993 4 0 0 25 0 1 0 474630561 8183808 1612 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1998 1612 603 41 0 1957 0 vsize: 7992 [startup+40.0006 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1634 0 0 0 3992 4 0 0 25 0 1 0 474630561 8183808 1612 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1998 1612 603 41 0 1957 0 vsize: 7992 [startup+50.001 s] Raw data (loadavg): 0.96 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1722 0 0 0 4992 5 0 0 25 0 1 0 474630561 8581120 1700 4294967295 134512640 134672761 3221224624 3221223728 134560194 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2095 1700 603 41 0 2054 0 vsize: 8380 [startup+60.001 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1855 0 0 0 5992 5 0 0 25 0 1 0 474630561 9121792 1833 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2227 1833 603 41 0 2186 0 vsize: 8908 [startup+70.001 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1855 0 0 0 6992 5 0 0 25 0 1 0 474630561 9121792 1833 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2227 1833 603 41 0 2186 0 vsize: 8908 [startup+80.0014 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1855 0 0 0 7992 5 0 0 25 0 1 0 474630561 9121792 1833 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2227 1833 603 41 0 2186 0 vsize: 8908 [startup+90.0012 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1879 0 0 0 8992 5 0 0 25 0 1 0 474630561 9252864 1857 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2259 1857 603 41 0 2218 0 vsize: 9036 [startup+100.001 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 1901 0 0 0 9992 5 0 0 25 0 1 0 474630561 9388032 1879 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2292 1879 603 41 0 2251 0 vsize: 9168 [startup+110.002 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2028 0 0 0 10991 6 0 0 25 0 1 0 474630561 9936896 2006 4294967295 134512640 134672761 3221224624 3221223728 134560477 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2006 603 41 0 2385 0 vsize: 9704 [startup+120.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2033 0 0 0 11991 6 0 0 25 0 1 0 474630561 9936896 2011 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2011 603 41 0 2385 0 vsize: 9704 [startup+130.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2033 0 0 0 12992 6 0 0 25 0 1 0 474630561 9936896 2011 4294967295 134512640 134672761 3221224624 3221223720 1075347141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2011 603 41 0 2385 0 vsize: 9704 [startup+140.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2033 0 0 0 13992 6 0 0 25 0 1 0 474630561 9936896 2011 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2011 603 41 0 2385 0 vsize: 9704 [startup+150.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2033 0 0 0 14992 6 0 0 25 0 1 0 474630561 9936896 2011 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2011 603 41 0 2385 0 vsize: 9704 [startup+160.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2033 0 0 0 15992 6 0 0 25 0 1 0 474630561 9936896 2011 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2011 603 41 0 2385 0 vsize: 9704 [startup+170.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2033 0 0 0 16992 6 0 0 25 0 1 0 474630561 9936896 2011 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2011 603 41 0 2385 0 vsize: 9704 [startup+180.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2034 0 0 0 17992 6 0 0 25 0 1 0 474630561 9936896 2012 4294967295 134512640 134672761 3221224624 3221223792 134560900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2012 603 41 0 2385 0 vsize: 9704 [startup+190.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2034 0 0 0 18992 6 0 0 25 0 1 0 474630561 9936896 2012 4294967295 134512640 134672761 3221224624 3221223808 134559663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2012 603 41 0 2385 0 vsize: 9704 [startup+200.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2034 0 0 0 19993 6 0 0 25 0 1 0 474630561 9936896 2012 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2012 603 41 0 2385 0 vsize: 9704 [startup+210.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2034 0 0 0 20993 6 0 0 25 0 1 0 474630561 9936896 2012 4294967295 134512640 134672761 3221224624 3221223760 134560686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2012 603 41 0 2385 0 vsize: 9704 [startup+220.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2034 0 0 0 21993 6 0 0 25 0 1 0 474630561 9936896 2012 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2012 603 41 0 2385 0 vsize: 9704 [startup+230.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2035 0 0 0 22993 6 0 0 25 0 1 0 474630561 9936896 2013 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2426 2013 603 41 0 2385 0 vsize: 9704 [startup+240.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2052 0 0 0 23993 7 0 0 25 0 1 0 474630561 10084352 2030 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2462 2030 603 41 0 2421 0 vsize: 9848 [startup+250.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2052 0 0 0 24993 7 0 0 25 0 1 0 474630561 10084352 2030 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2462 2030 603 41 0 2421 0 vsize: 9848 [startup+260.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2052 0 0 0 25993 7 0 0 25 0 1 0 474630561 10084352 2030 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2462 2030 603 41 0 2421 0 vsize: 9848 [startup+270.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2052 0 0 0 26993 7 0 0 25 0 1 0 474630561 10084352 2030 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2462 2030 603 41 0 2421 0 vsize: 9848 [startup+280.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2146 0 0 0 27993 7 0 0 25 0 1 0 474630561 10350592 2124 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2527 2124 603 41 0 2486 0 vsize: 10108 [startup+290.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2155 0 0 0 28993 7 0 0 25 0 1 0 474630561 10485760 2133 4294967295 134512640 134672761 3221224624 3221223808 134558667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2560 2133 603 41 0 2519 0 vsize: 10240 [startup+300.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2204 0 0 0 29993 8 0 0 25 0 1 0 474630561 10620928 2182 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2593 2182 603 41 0 2552 0 vsize: 10372 [startup+310.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2375 0 0 0 30993 8 0 0 25 0 1 0 474630561 11288576 2353 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2353 603 41 0 2715 0 vsize: 11024 [startup+320.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 31993 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+330.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 32993 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+340.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 33993 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+350.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 34993 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+360.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 35994 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223728 134560226 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+370.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 36994 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+380.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 37994 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+390.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 38994 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223760 134565098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+400.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 39994 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223760 134565096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+410.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2379 0 0 0 40994 8 0 0 25 0 1 0 474630561 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+420.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2420 0 0 0 41995 8 0 0 25 0 1 0 474630561 11558912 2398 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2822 2398 603 41 0 2781 0 vsize: 11288 [startup+430.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2428 0 0 0 42995 8 0 0 25 0 1 0 474630561 11558912 2406 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2822 2406 603 41 0 2781 0 vsize: 11288 [startup+440.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2522 0 0 0 43995 9 0 0 25 0 1 0 474630561 11956224 2500 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2919 2500 603 41 0 2878 0 vsize: 11676 [startup+450.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2531 0 0 0 44995 9 0 0 25 0 1 0 474630561 11956224 2509 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2919 2509 603 41 0 2878 0 vsize: 11676 [startup+460.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2538 0 0 0 45995 9 0 0 25 0 1 0 474630561 11956224 2516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2919 2516 603 41 0 2878 0 vsize: 11676 [startup+470.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2538 0 0 0 46995 9 0 0 25 0 1 0 474630561 11956224 2516 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2919 2516 603 41 0 2878 0 vsize: 11676 [startup+480.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2538 0 0 0 47995 9 0 0 25 0 1 0 474630561 11956224 2516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2919 2516 603 41 0 2878 0 vsize: 11676 [startup+490.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2628 0 0 0 48995 9 0 0 25 0 1 0 474630561 12357632 2606 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3017 2606 603 41 0 2976 0 vsize: 12068 [startup+500.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2722 0 0 0 49995 9 0 0 25 0 1 0 474630561 12750848 2700 4294967295 134512640 134672761 3221224624 3221223804 134553584 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3113 2700 603 41 0 3072 0 vsize: 12452 [startup+510.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2790 0 0 0 50995 10 0 0 25 0 1 0 474630561 13012992 2768 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3177 2768 603 41 0 3136 0 vsize: 12708 [startup+520.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2847 0 0 0 51995 10 0 0 25 0 1 0 474630561 13275136 2825 4294967295 134512640 134672761 3221224624 3221223544 1075351076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3241 2825 603 41 0 3200 0 vsize: 12964 [startup+530.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2858 0 0 0 52995 10 0 0 25 0 1 0 474630561 13275136 2836 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3241 2836 603 41 0 3200 0 vsize: 12964 [startup+540.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2869 0 0 0 53996 10 0 0 25 0 1 0 474630561 13418496 2847 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3276 2847 603 41 0 3235 0 vsize: 13104 [startup+550.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2883 0 0 0 54996 10 0 0 25 0 1 0 474630561 13418496 2861 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3276 2861 603 41 0 3235 0 vsize: 13104 [startup+560.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2939 0 0 0 55996 10 0 0 25 0 1 0 474630561 13684736 2917 4294967295 134512640 134672761 3221224624 3221223728 134560226 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3341 2917 603 41 0 3300 0 vsize: 13364 [startup+570.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2957 0 0 0 56996 10 0 0 25 0 1 0 474630561 13684736 2935 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3341 2935 603 41 0 3300 0 vsize: 13364 [startup+580.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2967 0 0 0 57996 10 0 0 25 0 1 0 474630561 13819904 2945 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2945 603 41 0 3333 0 vsize: 13496 [startup+590.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2969 0 0 0 58997 10 0 0 25 0 1 0 474630561 13819904 2947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2947 603 41 0 3333 0 vsize: 13496 [startup+600.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2982 0 0 0 59996 10 0 0 25 0 1 0 474630561 13819904 2960 4294967295 134512640 134672761 3221224624 3221223680 134565116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2960 603 41 0 3333 0 vsize: 13496 [startup+610.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 2987 0 0 0 60996 10 0 0 25 0 1 0 474630561 13819904 2965 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2965 603 41 0 3333 0 vsize: 13496 [startup+620.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3001 0 0 0 61996 10 0 0 25 0 1 0 474630561 13950976 2979 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3406 2979 603 41 0 3365 0 vsize: 13624 [startup+630.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3009 0 0 0 62996 10 0 0 25 0 1 0 474630561 13950976 2987 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3406 2987 603 41 0 3365 0 vsize: 13624 [startup+640.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3045 0 0 0 63996 10 0 0 25 0 1 0 474630561 14086144 3023 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3439 3023 603 41 0 3398 0 vsize: 13756 [startup+650.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3045 0 0 0 64997 10 0 0 25 0 1 0 474630561 14086144 3023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3439 3023 603 41 0 3398 0 vsize: 13756 [startup+660.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3088 0 0 0 65997 10 0 0 25 0 1 0 474630561 14241792 3066 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3477 3066 603 41 0 3436 0 vsize: 13908 [startup+670.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3095 0 0 0 66997 11 0 0 25 0 1 0 474630561 14381056 3073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3511 3073 603 41 0 3470 0 vsize: 14044 [startup+680.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3101 0 0 0 67997 11 0 0 25 0 1 0 474630561 14381056 3079 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3511 3079 603 41 0 3470 0 vsize: 14044 [startup+690.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3111 0 0 0 68997 11 0 0 25 0 1 0 474630561 14381056 3089 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3511 3089 603 41 0 3470 0 vsize: 14044 [startup+700.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3174 0 0 0 69997 11 0 0 25 0 1 0 474630561 14659584 3152 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3579 3152 603 41 0 3538 0 vsize: 14316 [startup+710.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3177 0 0 0 70997 11 0 0 25 0 1 0 474630561 14659584 3155 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3579 3155 603 41 0 3538 0 vsize: 14316 [startup+720.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3190 0 0 0 71997 11 0 0 25 0 1 0 474630561 14790656 3168 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3611 3168 603 41 0 3570 0 vsize: 14444 [startup+730.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3190 0 0 0 72997 11 0 0 25 0 1 0 474630561 14790656 3168 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3611 3168 603 41 0 3570 0 vsize: 14444 [startup+740.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3190 0 0 0 73997 11 0 0 25 0 1 0 474630561 14790656 3168 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3611 3168 603 41 0 3570 0 vsize: 14444 [startup+750.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3224 0 0 0 74997 11 0 0 25 0 1 0 474630561 14921728 3202 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3643 3202 603 41 0 3602 0 vsize: 14572 [startup+760.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3228 0 0 0 75997 11 0 0 25 0 1 0 474630561 14921728 3206 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3206 603 41 0 3602 0 vsize: 14572 [startup+770.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 76997 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223640 1075353067 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+780.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 77997 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+790.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 78997 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+800.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 79997 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+810.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 80997 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+820.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 81998 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+830.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 82998 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+840.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 83998 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+850.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 84998 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+860.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 85998 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+870.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 86998 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+880.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 87998 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+890.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 88999 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+900.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 89999 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+910.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3246 0 0 0 90999 12 0 0 25 0 1 0 474630561 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+920.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3247 0 0 0 91999 12 0 0 25 0 1 0 474630561 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3225 603 41 0 3602 0 vsize: 14572 [startup+930.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3247 0 0 0 92999 12 0 0 25 0 1 0 474630561 14921728 3225 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3225 603 41 0 3602 0 vsize: 14572 [startup+940.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3247 0 0 0 93999 12 0 0 25 0 1 0 474630561 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3225 603 41 0 3602 0 vsize: 14572 [startup+950.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3247 0 0 0 95000 12 0 0 25 0 1 0 474630561 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3225 603 41 0 3602 0 vsize: 14572 [startup+960.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3247 0 0 0 96000 12 0 0 25 0 1 0 474630561 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3225 603 41 0 3602 0 vsize: 14572 [startup+970.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3247 0 0 0 97000 12 0 0 25 0 1 0 474630561 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3225 603 41 0 3602 0 vsize: 14572 [startup+980.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 98000 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223776 134565080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+990.017 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 99001 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1000.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 100000 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1010.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 101001 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1020.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 102001 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223808 134559594 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1030.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 103001 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1040.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 104002 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1050.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 105002 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1060.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 106002 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1070.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 107002 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223808 134559532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1080.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 108002 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134553610 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1090.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 109002 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1100.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 110003 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1110.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 111003 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1120.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 112003 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1130.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 113003 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1140.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3248 0 0 0 114003 12 0 0 25 0 1 0 474630561 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+1150.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3310 0 0 0 115003 13 0 0 25 0 1 0 474630561 15187968 3288 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3708 3288 603 41 0 3667 0 vsize: 14832 [startup+1160.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3312 0 0 0 116003 13 0 0 25 0 1 0 474630561 15187968 3290 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3708 3290 603 41 0 3667 0 vsize: 14832 [startup+1170.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3320 0 0 0 117003 13 0 0 25 0 1 0 474630561 15319040 3298 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3740 3298 603 41 0 3699 0 vsize: 14960 [startup+1180.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3400 0 0 0 118003 13 0 0 25 0 1 0 474630561 15585280 3378 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3805 3378 603 41 0 3764 0 vsize: 15220 [startup+1190.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3408 0 0 0 119004 13 0 0 25 0 1 0 474630561 15585280 3386 4294967295 134512640 134672761 3221224624 3221223808 134558702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3805 3386 603 41 0 3764 0 vsize: 15220 [startup+1200.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 722 Raw data (stat): 722 (minisat+) R 721 26667 26666 0 -1 0 3414 0 0 0 120004 13 0 0 25 0 1 0 474630561 15720448 3392 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3838 3392 603 41 0 3797 0 vsize: 15352 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.03 s] Raw data (loadavg): 0.99 0.98 0.93 1/54 722 Raw data (stat): 722 (minisat+) Z 721 26667 26666 0 -1 12 3417 0 0 0 120004 13 0 0 25 0 1 0 474630561 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.03 CPU time (s): 1200.18 CPU user time (s): 1200.04 CPU system time (s): 0.137979 CPU usage (%): 100.012 Max. virtual memory (Kb): 15352 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####