Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-markshare1.opb |
MD5SUM | ba87f5dfbaed559dc55bc00bf07dc880 |
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.68 |
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 wulflinc6 THE 2005-04-21 13:41:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18504 boxname=wulflinc6 idbench=1424 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: ba87f5dfbaed559dc55bc00bf07dc880 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-markshare1.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-markshare1.opb IDLAUNCH: 18504 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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.042 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: 761920 kB Buffers: 29384 kB Cached: 222548 kB SwapCached: 552 kB Active: 36848 kB Inactive: 217144 kB HighTotal: 131008 kB HighFree: 36596 kB LowTotal: 903652 kB LowFree: 725324 kB SwapTotal: 2097136 kB SwapFree: 2095720 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5112 kB Slab: 13032 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 14:01:05 (client local time) WITH STATUS 10 IN 1200.35 SECONDS stats: 18504 7 1200.35 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.85 0.97 0.92 2/54 16735 Raw data (stat): 16735 (runsolver) R 16734 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487294756 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.87 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1244 0 0 0 994 4 0 0 25 0 1 0 487294756 6582272 1222 4294967295 134512640 134672761 3221224624 3221223760 134560598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1607 1222 603 41 0 1566 0 vsize: 6428 [startup+20.0002 s] Raw data (loadavg): 0.89 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1634 0 0 0 1993 6 0 0 25 0 1 0 487294756 8183808 1612 4294967295 134512640 134672761 3221224624 3221223924 134556634 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.0009 s] Raw data (loadavg): 0.91 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1634 0 0 0 2993 6 0 0 25 0 1 0 487294756 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+40.001 s] Raw data (loadavg): 0.92 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1634 0 0 0 3993 6 0 0 25 0 1 0 487294756 8183808 1612 4294967295 134512640 134672761 3221224624 3221223760 134565098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1998 1612 603 41 0 1957 0 vsize: 7992 [startup+50.0007 s] Raw data (loadavg): 0.93 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1709 0 0 0 4992 7 0 0 25 0 1 0 487294756 8581120 1687 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2095 1687 603 41 0 2054 0 vsize: 8380 [startup+60.0013 s] Raw data (loadavg): 0.94 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1855 0 0 0 5991 8 0 0 25 0 1 0 487294756 9121792 1833 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.0015 s] Raw data (loadavg): 0.95 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1855 0 0 0 6991 8 0 0 25 0 1 0 487294756 9121792 1833 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2227 1833 603 41 0 2186 0 vsize: 8908 [startup+80.0012 s] Raw data (loadavg): 0.96 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1855 0 0 0 7991 8 0 0 25 0 1 0 487294756 9121792 1833 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2227 1833 603 41 0 2186 0 vsize: 8908 [startup+90.0018 s] Raw data (loadavg): 0.96 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1879 0 0 0 8991 9 0 0 25 0 1 0 487294756 9252864 1857 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2259 1857 603 41 0 2218 0 vsize: 9036 [startup+100.002 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 1894 0 0 0 9991 9 0 0 25 0 1 0 487294756 9252864 1872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2259 1872 603 41 0 2218 0 vsize: 9036 [startup+110.002 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2028 0 0 0 10990 10 0 0 25 0 1 0 487294756 9936896 2006 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2426 2006 603 41 0 2385 0 vsize: 9704 [startup+120.002 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2033 0 0 0 11990 10 0 0 25 0 1 0 487294756 9936896 2011 4294967295 134512640 134672761 3221224624 3221223760 134565048 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.98 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2033 0 0 0 12990 10 0 0 25 0 1 0 487294756 9936896 2011 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.98 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2033 0 0 0 13990 10 0 0 25 0 1 0 487294756 9936896 2011 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.001 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2033 0 0 0 14990 10 0 0 25 0 1 0 487294756 9936896 2011 4294967295 134512640 134672761 3221224624 3221223792 134561021 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.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2033 0 0 0 15991 10 0 0 25 0 1 0 487294756 9936896 2011 4294967295 134512640 134672761 3221224624 3221223824 134557876 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.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2033 0 0 0 16991 10 0 0 25 0 1 0 487294756 9936896 2011 4294967295 134512640 134672761 3221224624 3221223788 134561235 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.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2034 0 0 0 17991 11 0 0 25 0 1 0 487294756 9936896 2012 4294967295 134512640 134672761 3221224624 3221223792 134561193 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.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2034 0 0 0 18991 11 0 0 25 0 1 0 487294756 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+200.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2034 0 0 0 19991 11 0 0 25 0 1 0 487294756 9936896 2012 4294967295 134512640 134672761 3221224624 3221223824 134557842 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 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2034 0 0 0 20991 11 0 0 25 0 1 0 487294756 9936896 2012 4294967295 134512640 134672761 3221224624 3221223792 134560830 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 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2034 0 0 0 21992 11 0 0 25 0 1 0 487294756 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 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2035 0 0 0 22992 11 0 0 25 0 1 0 487294756 9936896 2013 4294967295 134512640 134672761 3221224624 3221223760 134560566 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 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2052 0 0 0 23992 11 0 0 25 0 1 0 487294756 10084352 2030 4294967295 134512640 134672761 3221224624 3221223792 134560828 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 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2052 0 0 0 24993 11 0 0 25 0 1 0 487294756 10084352 2030 4294967295 134512640 134672761 3221224624 3221223792 134561151 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 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2052 0 0 0 25993 11 0 0 25 0 1 0 487294756 10084352 2030 4294967295 134512640 134672761 3221224624 3221223792 134561151 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 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2052 0 0 0 26993 11 0 0 25 0 1 0 487294756 10084352 2030 4294967295 134512640 134672761 3221224624 3221223808 134559031 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 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2149 0 0 0 27993 11 0 0 25 0 1 0 487294756 10350592 2127 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2527 2127 603 41 0 2486 0 vsize: 10108 [startup+290 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2204 0 0 0 28993 11 0 0 25 0 1 0 487294756 10620928 2182 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2593 2182 603 41 0 2552 0 vsize: 10372 [startup+300.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2231 0 0 0 29994 11 0 0 25 0 1 0 487294756 10756096 2209 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2626 2209 603 41 0 2585 0 vsize: 10504 [startup+310.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 30993 12 0 0 25 0 1 0 487294756 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+320.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 31994 12 0 0 25 0 1 0 487294756 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 32994 12 0 0 25 0 1 0 487294756 11288576 2357 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+340.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 33993 12 0 0 25 0 1 0 487294756 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+350.001 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 34993 12 0 0 25 0 1 0 487294756 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134560849 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.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 35993 12 0 0 25 0 1 0 487294756 11288576 2357 4294967295 134512640 134672761 3221224624 3221223624 1075350790 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.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 36994 12 0 0 25 0 1 0 487294756 11288576 2357 4294967295 134512640 134672761 3221224624 3221223808 134559345 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.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 37994 12 0 0 25 0 1 0 487294756 11288576 2357 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2756 2357 603 41 0 2715 0 vsize: 11024 [startup+390.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 38993 12 0 0 25 0 1 0 487294756 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+400.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2379 0 0 0 39994 12 0 0 25 0 1 0 487294756 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+410.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2413 0 0 0 40994 13 0 0 25 0 1 0 487294756 11423744 2391 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2789 2391 603 41 0 2748 0 vsize: 11156 [startup+420.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2421 0 0 0 41994 13 0 0 25 0 1 0 487294756 11558912 2399 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2822 2399 603 41 0 2781 0 vsize: 11288 [startup+430.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2432 0 0 0 42994 13 0 0 25 0 1 0 487294756 11558912 2410 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2822 2410 603 41 0 2781 0 vsize: 11288 [startup+440.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2522 0 0 0 43994 13 0 0 25 0 1 0 487294756 11956224 2500 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2535 0 0 0 44994 13 0 0 25 0 1 0 487294756 11956224 2513 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2919 2513 603 41 0 2878 0 vsize: 11676 [startup+460.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2538 0 0 0 45995 13 0 0 25 0 1 0 487294756 11956224 2516 4294967295 134512640 134672761 3221224624 3221223760 134560677 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.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2538 0 0 0 46995 13 0 0 25 0 1 0 487294756 11956224 2516 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2628 0 0 0 47995 14 0 0 25 0 1 0 487294756 12357632 2606 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3017 2606 603 41 0 2976 0 vsize: 12068 [startup+490.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2636 0 0 0 48996 14 0 0 25 0 1 0 487294756 12357632 2614 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3017 2614 603 41 0 2976 0 vsize: 12068 [startup+500.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2790 0 0 0 49995 14 0 0 25 0 1 0 487294756 13012992 2768 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3177 2768 603 41 0 3136 0 vsize: 12708 [startup+510.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2800 0 0 0 50995 14 0 0 25 0 1 0 487294756 13012992 2778 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3177 2778 603 41 0 3136 0 vsize: 12708 [startup+520.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2847 0 0 0 51995 15 0 0 25 0 1 0 487294756 13275136 2825 4294967295 134512640 134672761 3221224624 3221223792 134561003 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.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2869 0 0 0 52996 15 0 0 25 0 1 0 487294756 13418496 2847 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3276 2847 603 41 0 3235 0 vsize: 13104 [startup+540.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2879 0 0 0 53996 15 0 0 25 0 1 0 487294756 13418496 2857 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3276 2857 603 41 0 3235 0 vsize: 13104 [startup+550.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2939 0 0 0 54996 15 0 0 25 0 1 0 487294756 13684736 2917 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3341 2917 603 41 0 3300 0 vsize: 13364 [startup+560.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2945 0 0 0 55996 15 0 0 25 0 1 0 487294756 13684736 2923 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3341 2923 603 41 0 3300 0 vsize: 13364 [startup+570.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2967 0 0 0 56996 15 0 0 25 0 1 0 487294756 13819904 2945 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2945 603 41 0 3333 0 vsize: 13496 [startup+580.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2967 0 0 0 57997 15 0 0 25 0 1 0 487294756 13819904 2945 4294967295 134512640 134672761 3221224624 3221223792 134560888 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.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2982 0 0 0 58997 15 0 0 25 0 1 0 487294756 13819904 2960 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2960 603 41 0 3333 0 vsize: 13496 [startup+600.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 2985 0 0 0 59997 16 0 0 25 0 1 0 487294756 13819904 2963 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2963 603 41 0 3333 0 vsize: 13496 [startup+610.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3001 0 0 0 60998 16 0 0 25 0 1 0 487294756 13950976 2979 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3406 2979 603 41 0 3365 0 vsize: 13624 [startup+620.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3009 0 0 0 61998 16 0 0 25 0 1 0 487294756 13950976 2987 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3406 2987 603 41 0 3365 0 vsize: 13624 [startup+630.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3045 0 0 0 62998 16 0 0 25 0 1 0 487294756 14086144 3023 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3439 3023 603 41 0 3398 0 vsize: 13756 [startup+640.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3045 0 0 0 63998 16 0 0 25 0 1 0 487294756 14086144 3023 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3085 0 0 0 64999 16 0 0 25 0 1 0 487294756 14241792 3063 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3477 3063 603 41 0 3436 0 vsize: 13908 [startup+660.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3093 0 0 0 65999 16 0 0 25 0 1 0 487294756 14241792 3071 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3477 3071 603 41 0 3436 0 vsize: 13908 [startup+670.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3101 0 0 0 66999 16 0 0 25 0 1 0 487294756 14381056 3079 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3511 3079 603 41 0 3470 0 vsize: 14044 [startup+680.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3111 0 0 0 68000 16 0 0 25 0 1 0 487294756 14381056 3089 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3511 3089 603 41 0 3470 0 vsize: 14044 [startup+690.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3174 0 0 0 69000 16 0 0 25 0 1 0 487294756 14659584 3152 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3579 3152 603 41 0 3538 0 vsize: 14316 [startup+700.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3177 0 0 0 70000 16 0 0 25 0 1 0 487294756 14659584 3155 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3579 3155 603 41 0 3538 0 vsize: 14316 [startup+710.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3190 0 0 0 71000 16 0 0 25 0 1 0 487294756 14790656 3168 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3611 3168 603 41 0 3570 0 vsize: 14444 [startup+720.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3190 0 0 0 72001 16 0 0 25 0 1 0 487294756 14790656 3168 4294967295 134512640 134672761 3221224624 3221223792 134561154 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.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3190 0 0 0 73001 16 0 0 25 0 1 0 487294756 14790656 3168 4294967295 134512640 134672761 3221224624 3221223808 134559340 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.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3224 0 0 0 74001 17 0 0 25 0 1 0 487294756 14921728 3202 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3643 3202 603 41 0 3602 0 vsize: 14572 [startup+750.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3228 0 0 0 75001 17 0 0 25 0 1 0 487294756 14921728 3206 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3206 603 41 0 3602 0 vsize: 14572 [startup+760.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 76001 17 0 0 25 0 1 0 487294756 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3224 603 41 0 3602 0 vsize: 14572 [startup+770.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 77001 17 0 0 25 0 1 0 487294756 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+780.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 78002 17 0 0 25 0 1 0 487294756 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134561003 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.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 79002 17 0 0 25 0 1 0 487294756 14921728 3224 4294967295 134512640 134672761 3221224624 3221223776 134565137 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.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 80002 17 0 0 25 0 1 0 487294756 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560940 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.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 81002 17 0 0 25 0 1 0 487294756 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+820.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 82003 17 0 0 25 0 1 0 487294756 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.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 83003 17 0 0 25 0 1 0 487294756 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134561533 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.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 84004 17 0 0 25 0 1 0 487294756 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.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 85004 17 0 0 25 0 1 0 487294756 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 86004 17 0 0 25 0 1 0 487294756 14921728 3224 4294967295 134512640 134672761 3221224624 3221223824 134557836 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.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 87004 17 0 0 25 0 1 0 487294756 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.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 88005 17 0 0 25 0 1 0 487294756 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+890.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 89005 17 0 0 25 0 1 0 487294756 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+900.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3246 0 0 0 90006 17 0 0 25 0 1 0 487294756 14921728 3224 4294967295 134512640 134672761 3221224624 3221223792 134561008 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3247 0 0 0 91006 17 0 0 25 0 1 0 487294756 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3225 603 41 0 3602 0 vsize: 14572 [startup+920.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3247 0 0 0 92006 17 0 0 25 0 1 0 487294756 14921728 3225 4294967295 134512640 134672761 3221224624 3221223808 134559489 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3247 0 0 0 93006 17 0 0 25 0 1 0 487294756 14921728 3225 4294967295 134512640 134672761 3221224624 3221223824 134557836 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3247 0 0 0 94007 17 0 0 25 0 1 0 487294756 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134561016 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3247 0 0 0 95007 17 0 0 25 0 1 0 487294756 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134560874 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3247 0 0 0 96007 17 0 0 25 0 1 0 487294756 14921728 3225 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 97007 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223632 134565852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3643 3226 603 41 0 3602 0 vsize: 14572 [startup+980.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 98008 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134561198 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.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 99008 18 0 0 25 0 1 0 487294756 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 100008 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134561190 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 101009 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560980 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 102009 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560948 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 103009 18 0 0 25 0 1 0 487294756 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+1040.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 104010 18 0 0 25 0 1 0 487294756 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 105010 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223748 134566118 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 106010 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134561118 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 107011 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560852 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 108011 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223768 134560630 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 109011 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560858 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 110011 18 0 0 25 0 1 0 487294756 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+1110.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 111012 18 0 0 25 0 1 0 487294756 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+1120.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3248 0 0 0 112012 18 0 0 25 0 1 0 487294756 14921728 3226 4294967295 134512640 134672761 3221224624 3221223792 134560876 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.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3308 0 0 0 113012 18 0 0 25 0 1 0 487294756 15187968 3286 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3708 3286 603 41 0 3667 0 vsize: 14832 [startup+1140.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16735 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3310 0 0 0 114013 18 0 0 25 0 1 0 487294756 15187968 3288 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3708 3288 603 41 0 3667 0 vsize: 14832 [startup+1150.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16788 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3317 0 0 0 115013 18 0 0 25 0 1 0 487294756 15319040 3295 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3740 3295 603 41 0 3699 0 vsize: 14960 [startup+1160.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16788 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3327 0 0 0 116013 19 0 0 25 0 1 0 487294756 15319040 3305 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3740 3305 603 41 0 3699 0 vsize: 14960 [startup+1170.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16788 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3408 0 0 0 117013 19 0 0 25 0 1 0 487294756 15585280 3386 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3805 3386 603 41 0 3764 0 vsize: 15220 [startup+1180.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16788 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3411 0 0 0 118014 19 0 0 25 0 1 0 487294756 15720448 3389 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3838 3389 603 41 0 3797 0 vsize: 15352 [startup+1190.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16788 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3414 0 0 0 119014 19 0 0 25 0 1 0 487294756 15720448 3392 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3838 3392 603 41 0 3797 0 vsize: 15352 [startup+1200.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 16788 Raw data (stat): 16735 (minisat+) R 16734 29653 29652 0 -1 0 3414 0 0 0 120014 19 0 0 25 0 1 0 487294756 15720448 3392 4294967295 134512640 134672761 3221224624 3221223792 134561008 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.97 0.92 1/54 16788 Raw data (stat): 16735 (minisat+) Z 16734 29653 29652 0 -1 12 3417 0 0 0 120014 19 0 0 25 0 1 0 487294756 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.35 CPU user time (s): 1200.15 CPU system time (s): 0.199969 CPU usage (%): 100.027 Max. virtual memory (Kb): 15352 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####