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 wulflinc12 THE 2005-05-25 23:07:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22608 boxname=wulflinc12 idbench=1424 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: ba87f5dfbaed559dc55bc00bf07dc880 /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-markshare1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-markshare1.opb IDLAUNCH: 22608 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 557436 kB Buffers: 34204 kB Cached: 421384 kB SwapCached: 488 kB Active: 22316 kB Inactive: 435596 kB HighTotal: 131008 kB HighFree: 17388 kB LowTotal: 903652 kB LowFree: 540048 kB SwapTotal: 2097136 kB SwapFree: 2096076 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5680 kB Slab: 13516 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 23:28:06 (client local time) WITH STATUS 152 IN 1229.84 SECONDS stats: 22608 7 1229.84 152 #### 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 % | c | 935718 | 14790 50045 | 24948 23120 980742 42.4 | 11.705 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 17489 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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.92 0.95 0.90 2/54 17485 Raw data (stat): 17485 (runsolver) R 17484 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784487866 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 0.93 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0003 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0011 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0006 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0018 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0019 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0022 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0037 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0041 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.005 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.71 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 17489 Raw data (stat): 17485 (minisat+_script) S 17484 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784487866 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.71 CPU time (s): 1229.84 CPU user time (s): 1229.67 CPU system time (s): 0.171973 CPU usage (%): 100.011 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####