Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare1.opb |
MD5SUM | 6f06e375914e0285ec75de90ad627758 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3712 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 120 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 6291450 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 6291450 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.1 |
Number of variables | 170 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 70 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc12 THE 2005-04-21 16:03:24 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17638 boxname=wulflinc12 idbench=1357 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6f06e375914e0285ec75de90ad627758 /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-markshare1.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-markshare1.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-markshare1.opb IDLAUNCH: 17638 /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: 776832 kB Buffers: 26260 kB Cached: 210212 kB SwapCached: 508 kB Active: 50800 kB Inactive: 187792 kB HighTotal: 131008 kB HighFree: 32564 kB LowTotal: 903652 kB LowFree: 744268 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5276 kB Slab: 13640 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 16:23:26 (client local time) WITH STATUS 10 IN 1200.18 SECONDS stats: 17638 7 1200.18 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 12 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 10]---> Adder-cost: 304 maxlim: 405119 bits: 20/19 c ---[ 8]---> Adder-cost: 314 maxlim: 431743 bits: 20/19 c ---[ 6]---> Adder-cost: 348 maxlim: 435327 bits: 20/19 c ---[ 4]---> Adder-cost: 318 maxlim: 411775 bits: 20/19 c ---[ 2]---> Adder-cost: 312 maxlim: 410751 bits: 20/19 c ---[ 0]---> Adder-cost: 314 maxlim: 411135 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 12820 45524 | 4273 0 0 nan | 0.000 % | c | 100 | 12820 45524 | 4700 100 583 5.8 | 11.212 % | c ============================================================================== c [1mFound solution: 511232[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 110 maxlim: 8288 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115 | 13523 48038 | 4507 115 713 6.2 | 11.212 % | c | 215 | 13515 48012 | 4957 214 5912 27.6 | 11.010 % | c ============================================================================== c [1mFound solution: 503680[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8347 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 348 | 13531 48096 | 4510 347 16026 46.2 | 11.010 % | c | 448 | 13523 48070 | 4961 446 28545 64.0 | 11.207 % | c | 599 | 13523 48070 | 5457 597 42809 71.7 | 11.207 % | c | 824 | 13523 48070 | 6002 822 66235 80.6 | 11.207 % | c ============================================================================== c [1mFound solution: 456704[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8714 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1042 | 13535 48141 | 4511 1040 75625 72.7 | 11.207 % | c ============================================================================== c [1mFound solution: 455808[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8721 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1079 | 13538 48164 | 4512 1077 77579 72.0 | 11.207 % | c | 1179 | 13538 48164 | 4963 1177 88739 75.4 | 11.432 % | c | 1329 | 13538 48164 | 5459 1327 105274 79.3 | 11.432 % | c | 1556 | 13538 48164 | 6005 1554 122467 78.8 | 11.432 % | c | 1894 | 13538 48164 | 6606 1892 144685 76.5 | 11.432 % | c ============================================================================== c [1mFound solution: 383232[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 9288 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2069 | 13549 48219 | 4516 2067 159419 77.1 | 11.432 % | c | 2169 | 13549 48219 | 4967 2167 169791 78.4 | 11.570 % | c | 2321 | 13549 48219 | 5464 2319 185407 80.0 | 11.570 % | c | 2548 | 13549 48219 | 6010 2546 200655 78.8 | 11.570 % | c | 2885 | 13549 48219 | 6611 2883 229403 79.6 | 11.570 % | c | 3391 | 13549 48219 | 7273 3389 265847 78.4 | 11.570 % | c | 4150 | 13533 48167 | 8000 4146 321237 77.5 | 11.656 % | c ============================================================================== c [1mFound solution: 364288[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 9436 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4517 | 13544 48235 | 4514 4513 356795 79.1 | 11.656 % | c | 4618 | 13544 48235 | 4965 4614 368915 80.0 | 11.868 % | c | 4768 | 13544 48235 | 5461 4764 379005 79.6 | 11.868 % | c | 4994 | 13544 48235 | 6008 4990 390119 78.2 | 11.868 % | c | 5332 | 13544 48235 | 6608 5328 416527 78.2 | 11.868 % | c | 5838 | 13544 48235 | 7269 5834 458111 78.5 | 11.868 % | c | 6597 | 13544 48235 | 7996 6593 514456 78.0 | 11.868 % | c | 7736 | 13544 48235 | 8796 7732 587098 75.9 | 11.868 % | c | 9445 | 13536 48209 | 9676 9440 719576 76.2 | 11.911 % | c | 12009 | 13528 48183 | 10643 6758 492981 72.9 | 11.954 % | c | 15853 | 13528 48183 | 11708 10602 783975 73.9 | 11.954 % | c | 21619 | 13514 48143 | 12878 9988 709104 71.0 | 12.082 % | c ============================================================================== c [1mFound solution: 335360[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 9662 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23589 | 13527 48235 | 4509 11958 863512 72.2 | 12.082 % | c | 23690 | 13527 48235 | 4959 3091 167808 54.3 | 12.377 % | c | 23842 | 13527 48235 | 5455 3243 175273 54.0 | 12.377 % | c | 24067 | 13527 48235 | 6001 3468 196191 56.6 | 12.377 % | c | 24406 | 13527 48235 | 6601 3807 218204 57.3 | 12.377 % | c | 24912 | 13519 48209 | 7261 4312 254982 59.1 | 12.420 % | c | 25672 | 13511 48183 | 7987 5071 316388 62.4 | 12.463 % | c | 26811 | 13503 48157 | 8786 6209 386730 62.3 | 12.505 % | c ============================================================================== c [1mFound solution: 310016[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 9860 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27516 | 13500 48167 | 4500 6913 429968 62.2 | 12.505 % | c | 27617 | 13500 48167 | 4950 3558 171002 48.1 | 12.692 % | c | 27767 | 13500 48167 | 5445 3708 187587 50.6 | 12.692 % | c | 27992 | 13500 48167 | 5989 3933 206290 52.5 | 12.692 % | c | 28330 | 13500 48167 | 6588 4271 228093 53.4 | 12.692 % | c | 28836 | 13500 48167 | 7247 4777 268210 56.1 | 12.692 % | c | 29597 | 13500 48167 | 7972 5538 303899 54.9 | 12.692 % | c | 30738 | 13500 48167 | 8769 6679 359293 53.8 | 12.692 % | c | 32446 | 13492 48141 | 9646 8386 462548 55.2 | 12.734 % | c | 35008 | 13492 48141 | 10610 5647 368183 65.2 | 12.734 % | c ============================================================================== c [1mFound solution: 267904[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 10189 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37998 | 13500 48195 | 4500 8637 496764 57.5 | 12.734 % | c | 38098 | 13500 48195 | 4950 4419 149234 33.8 | 12.946 % | c | 38248 | 13500 48195 | 5445 4569 163668 35.8 | 12.946 % | c | 38475 | 13500 48195 | 5989 4796 181974 37.9 | 12.946 % | c | 38814 | 13500 48195 | 6588 5135 205638 40.0 | 12.946 % | c | 39321 | 13500 48195 | 7247 5642 238996 42.4 | 12.946 % | c | 40080 | 13500 48195 | 7972 6401 299534 46.8 | 12.946 % | c | 41219 | 13500 48195 | 8769 7540 385271 51.1 | 12.946 % | c | 42928 | 13500 48195 | 9646 9249 523733 56.6 | 12.946 % | c | 45490 | 13500 48195 | 10610 6515 412888 63.4 | 12.946 % | c | 49336 | 13492 48173 | 11671 10360 589091 56.9 | 13.031 % | c | 55102 | 13492 48173 | 12839 9980 406807 40.8 | 13.031 % | c ============================================================================== c [1mFound solution: 236544[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 10434 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 55890 | 13459 47854 | 4486 10768 442603 41.1 | 13.031 % | c | 55990 | 13459 47854 | 4934 2792 75560 27.1 | 13.235 % | c | 56140 | 13444 47801 | 5428 2934 82471 28.1 | 13.319 % | c | 56365 | 13444 47801 | 5970 3159 96705 30.6 | 13.319 % | c | 56702 | 13444 47801 | 6567 3496 115463 33.0 | 13.319 % | c | 57209 | 13444 47801 | 7224 4003 138314 34.6 | 13.319 % | c | 57970 | 13444 47801 | 7947 4764 173787 36.5 | 13.319 % | c ============================================================================== c [1mFound solution: 186112[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 10828 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 58797 | 13444 47817 | 4481 5586 219549 39.3 | 13.319 % | c | 58897 | 13444 47817 | 4929 2893 93209 32.2 | 13.564 % | c | 59048 | 13435 47788 | 5422 3042 97224 32.0 | 13.648 % | c | 59274 | 13435 47788 | 5964 3268 106868 32.7 | 13.648 % | c | 59611 | 13429 47770 | 6560 3604 117186 32.5 | 13.690 % | c | 60117 | 13429 47770 | 7216 4110 131247 31.9 | 13.690 % | c | 60876 | 13429 47770 | 7938 4869 162338 33.3 | 13.690 % | c ============================================================================== c [1mFound solution: 169088[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 10961 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 61287 | 13437 47807 | 4479 5280 193520 36.7 | 13.690 % | c | 61388 | 13437 47807 | 4926 2741 82723 30.2 | 13.812 % | c | 61538 | 13437 47807 | 5419 2891 90565 31.3 | 13.812 % | c | 61765 | 13437 47807 | 5961 3118 97940 31.4 | 13.812 % | c | 62103 | 13437 47807 | 6557 3456 112599 32.6 | 13.812 % | c | 62609 | 13437 47807 | 7213 3962 130470 32.9 | 13.812 % | c | 63368 | 13437 47807 | 7934 4721 176909 37.5 | 13.812 % | c ============================================================================== c [1mFound solution: 166400[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 10982 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 63847 | 13443 47851 | 4481 5200 192470 37.0 | 13.812 % | c | 63950 | 13443 47851 | 4929 2703 77060 28.5 | 13.945 % | c | 64100 | 13443 47851 | 5422 2853 81016 28.4 | 13.945 % | c | 64327 | 13443 47851 | 5964 3080 92806 30.1 | 13.945 % | c | 64664 | 13443 47851 | 6560 3417 104060 30.5 | 13.945 % | c | 65171 | 13443 47851 | 7216 3924 120099 30.6 | 13.945 % | c | 65930 | 13443 47851 | 7938 4683 138645 29.6 | 13.945 % | c | 67070 | 13443 47851 | 8732 5823 220994 38.0 | 13.945 % | c | 68779 | 13443 47851 | 9605 7532 340196 45.2 | 13.945 % | c | 71342 | 13443 47851 | 10565 10095 460397 45.6 | 13.945 % | c | 75186 | 13443 47851 | 11622 8193 314714 38.4 | 13.945 % | c | 80952 | 13443 47851 | 12784 7850 280319 35.7 | 13.945 % | c | 89601 | 13443 47851 | 14063 9855 407122 41.3 | 13.945 % | c ============================================================================== c [1mFound solution: 134528[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 11231 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 98628 | 13450 47879 | 4483 11452 464871 40.6 | 13.945 % | c | 98729 | 13450 47879 | 4931 2964 88892 30.0 | 14.071 % | c | 98879 | 13450 47879 | 5424 3114 91355 29.3 | 14.071 % | c | 99105 | 13450 47879 | 5966 3340 97831 29.3 | 14.071 % | c | 99442 | 13450 47879 | 6563 3677 109728 29.8 | 14.071 % | c | 99949 | 13450 47879 | 7219 4184 125717 30.0 | 14.071 % | c ============================================================================== c [1mFound solution: 123392[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 4 maxlim: 5174 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 100664 | 13395 47709 | 4465 4622 130720 28.3 | 14.071 % | c ============================================================================== c [1mFound solution: 117760[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5218 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 100728 | 13402 47743 | 4467 4686 131777 28.1 | 14.071 % | c | 100828 | 13391 47702 | 4913 4784 134201 28.1 | 14.907 % | c | 100978 | 13391 47702 | 5405 4934 136219 27.6 | 14.907 % | c | 101203 | 13391 47702 | 5945 5159 144607 28.0 | 14.907 % | c | 101542 | 13391 47702 | 6540 5498 155686 28.3 | 14.907 % | c | 102048 | 13354 47507 | 7194 5601 151869 27.1 | 15.072 % | c | 102807 | 13354 47507 | 7913 6360 181702 28.6 | 15.072 % | c | 103948 | 13338 47455 | 8704 7493 219839 29.3 | 15.197 % | c | 105656 | 13338 47455 | 9575 9201 289083 31.4 | 15.197 % | c | 108219 | 13338 47455 | 10532 6484 225564 34.8 | 15.197 % | c | 112064 | 13338 47455 | 11586 10329 392557 38.0 | 15.197 % | c | 117833 | 13338 47455 | 12744 9964 395569 39.7 | 15.197 % | c | 126482 | 13338 47455 | 14019 11834 494903 41.8 | 15.197 % | c ============================================================================== c [1mFound solution: 91648[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5422 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 135255 | 13348 47508 | 4449 13259 550001 41.5 | 15.197 % | c | 135355 | 13348 47508 | 4893 3415 93444 27.4 | 15.381 % | c | 135505 | 13348 47508 | 5383 3565 97087 27.2 | 15.381 % | c | 135731 | 13348 47508 | 5921 3791 103170 27.2 | 15.381 % | c | 136070 | 13348 47508 | 6513 4130 112364 27.2 | 15.381 % | c | 136577 | 13348 47508 | 7165 4637 129588 27.9 | 15.381 % | c | 137336 | 13348 47508 | 7881 5396 151242 28.0 | 15.381 % | c | 138478 | 13348 47508 | 8669 6538 200453 30.7 | 15.381 % | c | 140187 | 13348 47508 | 9536 8247 252593 30.6 | 15.381 % | c | 142750 | 13348 47508 | 10490 5608 166009 29.6 | 15.381 % | c | 146596 | 13348 47508 | 11539 9454 346848 36.7 | 15.381 % | c | 152363 | 13348 47508 | 12693 9129 346264 37.9 | 15.381 % | c | 161014 | 13348 47508 | 13962 11122 472397 42.5 | 15.381 % | c | 173988 | 13348 47508 | 15359 9531 331705 34.8 | 15.381 % | c ============================================================================== c [1mFound solution: 89984[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5435 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 192469 | 13354 47536 | 4451 11937 509956 42.7 | 15.381 % | c | 192570 | 13354 47536 | 4896 3086 85947 27.9 | 15.467 % | c | 192720 | 13354 47536 | 5385 3236 90181 27.9 | 15.467 % | c | 192945 | 13354 47536 | 5924 3461 98564 28.5 | 15.467 % | c | 193284 | 13354 47536 | 6516 3800 110407 29.1 | 15.467 % | c | 193790 | 13354 47536 | 7168 4306 125669 29.2 | 15.467 % | c | 194551 | 13354 47536 | 7885 5067 153749 30.3 | 15.467 % | c | 195690 | 13354 47536 | 8673 6206 191097 30.8 | 15.467 % | c | 197399 | 13354 47536 | 9541 7915 250712 31.7 | 15.467 % | c | 199962 | 13354 47536 | 10495 5375 158830 29.5 | 15.467 % | c | 203809 | 13354 47536 | 11544 9222 303039 32.9 | 15.467 % | c | 209575 | 13354 47536 | 12699 8805 337160 38.3 | 15.467 % | c | 218224 | 13346 47514 | 13969 10753 404450 37.6 | 15.549 % | c | 231198 | 13346 47514 | 15366 9195 348803 37.9 | 15.549 % | c | 250659 | 13346 47514 | 16902 12714 512087 40.3 | 15.549 % | c | 279852 | 13346 47514 | 18592 15680 673771 43.0 | 15.549 % | c ============================================================================== c [1mFound solution: 88832[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5444 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 288212 | 13351 47541 | 4450 14437 674320 46.7 | 15.549 % | c | 288313 | 13351 47541 | 4895 3711 145326 39.2 | 15.640 % | c | 288463 | 13351 47541 | 5384 3861 150549 39.0 | 15.640 % | c | 288688 | 13351 47541 | 5922 4086 157832 38.6 | 15.640 % | c | 289025 | 13351 47541 | 6515 4423 162657 36.8 | 15.640 % | c | 289531 | 13351 47541 | 7166 4929 176529 35.8 | 15.640 % | c | 290290 | 13351 47541 | 7883 5688 198324 34.9 | 15.640 % | c | 291429 | 13351 47541 | 8671 6827 236374 34.6 | 15.640 % | c | 293137 | 13351 47541 | 9538 8535 286968 33.6 | 15.640 % | c | 295700 | 13351 47541 | 10492 6071 161451 26.6 | 15.640 % | c ============================================================================== c [1mFound solution: 80256[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5511 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 297816 | 13355 47556 | 4451 8187 245635 30.0 | 15.640 % | c | 297916 | 13355 47556 | 4896 4194 117409 28.0 | 15.697 % | c | 298066 | 13355 47556 | 5385 4344 123164 28.4 | 15.697 % | c | 298291 | 13355 47556 | 5924 4569 130310 28.5 | 15.697 % | c | 298628 | 13355 47556 | 6516 4906 136788 27.9 | 15.697 % | c | 299135 | 13355 47556 | 7168 5413 150881 27.9 | 15.697 % | c | 299894 | 13355 47556 | 7885 6172 175794 28.5 | 15.697 % | c | 301033 | 13355 47556 | 8673 7311 210621 28.8 | 15.697 % | c | 302743 | 13355 47556 | 9541 9021 283371 31.4 | 15.697 % | c | 305305 | 13355 47556 | 10495 6346 245744 38.7 | 15.697 % | c | 309149 | 13355 47556 | 11544 10190 400207 39.3 | 15.697 % | c | 314915 | 13355 47556 | 12699 9896 369446 37.3 | 15.697 % | c | 323564 | 13355 47556 | 13969 11800 470407 39.9 | 15.697 % | c ============================================================================== c [1mFound solution: 77696[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5531 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 323896 | 13361 47582 | 4453 12132 482262 39.8 | 15.697 % | c | 323996 | 13361 47582 | 4898 3133 75277 24.0 | 15.781 % | c | 324147 | 13361 47582 | 5388 3284 77495 23.6 | 15.781 % | c | 324372 | 13361 47582 | 5926 3509 85920 24.5 | 15.781 % | c | 324709 | 13361 47582 | 6519 3846 94916 24.7 | 15.781 % | c | 325215 | 13361 47582 | 7171 4352 108935 25.0 | 15.781 % | c | 325974 | 13361 47582 | 7888 5111 130728 25.6 | 15.781 % | c | 327114 | 13361 47582 | 8677 6251 172348 27.6 | 15.781 % | c | 328822 | 13361 47582 | 9545 7959 248681 31.2 | 15.781 % | c | 331385 | 13361 47582 | 10499 5461 166076 30.4 | 15.781 % | c | 335229 | 13361 47582 | 11549 9305 299126 32.1 | 15.781 % | c | 340995 | 13361 47582 | 12704 8967 303099 33.8 | 15.781 % | c ============================================================================== c [1mFound solution: 60288[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 4 maxlim: 2595 bits: 12/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 341618 | 13302 47370 | 4434 9558 325905 34.1 | 15.781 % | c | 341718 | 13302 47370 | 4877 4879 155431 31.9 | 16.334 % | c | 341868 | 13302 47370 | 5365 5029 156993 31.2 | 16.334 % | c | 342093 | 13275 47277 | 5901 5242 160804 30.7 | 16.497 % | c | 342431 | 13275 47277 | 6491 5580 169155 30.3 | 16.497 % | c | 342937 | 13267 47251 | 7141 6085 179252 29.5 | 16.538 % | c | 343697 | 13267 47251 | 7855 6845 211486 30.9 | 16.538 % | c | 344837 | 13259 47225 | 8640 7984 255826 32.0 | 16.578 % | c | 346545 | 13215 46982 | 9504 4973 144117 29.0 | 16.741 % | c | 349107 | 13215 46982 | 10455 7535 229056 30.4 | 16.741 % | c | 352951 | 13215 46982 | 11500 5815 202197 34.8 | 16.741 % | c | 358719 | 13215 46982 | 12650 11583 441948 38.2 | 16.741 % | c | 367370 | 13215 46982 | 13915 6787 268985 39.6 | 16.741 % | c | 380344 | 13215 46982 | 15307 12510 492631 39.4 | 16.741 % | c | 399806 | 13215 46982 | 16838 15888 743079 46.8 | 16.741 % | c | 429001 | 13215 46982 | 18521 10073 395146 39.2 | 16.741 % | c | 472791 | 13215 46982 | 20374 15523 603968 38.9 | 16.741 % | c ============================================================================== c [1mFound solution: 56192[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2627 bits: 12/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 489177 | 13218 46993 | 4406 10691 473881 44.3 | 16.741 % | c | 489280 | 13218 46993 | 4846 2776 72406 26.1 | 16.802 % | c | 489432 | 13218 46993 | 5331 2928 74360 25.4 | 16.802 % | c | 489658 | 13218 46993 | 5864 3154 82687 26.2 | 16.802 % | c | 489995 | 13218 46993 | 6450 3491 92147 26.4 | 16.802 % | c | 490502 | 13218 46993 | 7095 3998 106587 26.7 | 16.802 % | c | 491262 | 13218 46993 | 7805 4758 125654 26.4 | 16.802 % | c | 492402 | 13218 46993 | 8586 5898 161958 27.5 | 16.802 % | c | 494111 | 13218 46993 | 9444 7607 224840 29.6 | 16.802 % | c | 496673 | 13218 46993 | 10389 10169 349191 34.3 | 16.802 % | c | 500518 | 13218 46993 | 11428 8485 308401 36.3 | 16.802 % | c | 506284 | 13218 46993 | 12570 8255 288221 34.9 | 16.802 % | c | 514936 | 13218 46993 | 13827 10266 360206 35.1 | 16.802 % | c | 527910 | 13218 46993 | 15210 8773 363496 41.4 | 16.802 % | c | 547372 | 13218 46993 | 16731 12366 499923 40.4 | 16.802 % | c | 576566 | 13218 46993 | 18404 15245 713837 46.8 | 16.802 % | c | 620356 | 13218 46993 | 20245 11197 382326 34.1 | 16.802 % | c ============================================================================== c [1mFound solution: 49152[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2682 bits: 12/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 650971 | 13227 47037 | 4409 20824 948231 45.5 | 16.802 % | c | 651072 | 13227 47037 | 4849 2704 61854 22.9 | 16.944 % | c | 651224 | 13227 47037 | 5334 2856 64619 22.6 | 16.944 % | c | 651452 | 13227 47037 | 5868 3084 71938 23.3 | 16.944 % | c | 651790 | 13227 47037 | 6455 3422 80852 23.6 | 16.944 % | c | 652297 | 13227 47037 | 7100 3929 97200 24.7 | 16.944 % | c | 653056 | 13227 47037 | 7810 4688 124393 26.5 | 16.944 % | c | 654195 | 13227 47037 | 8591 5827 164767 28.3 | 16.944 % | c | 655903 | 13227 47037 | 9451 7535 259879 34.5 | 16.944 % | c | 658466 | 13227 47037 | 10396 10098 370855 36.7 | 16.944 % | c | 662310 | 13227 47037 | 11435 8387 320102 38.2 | 16.944 % | c | 668076 | 13227 47037 | 12579 8114 267287 32.9 | 16.944 % | c | 676725 | 13227 47037 | 13837 10194 339745 33.3 | 16.944 % | c | 689699 | 13227 47037 | 15221 8669 314640 36.3 | 16.944 % | c | 709160 | 13227 47037 | 16743 12252 577429 47.1 | 16.944 % | c ============================================================================== c [1mFound solution: 39040[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2761 bits: 12/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 718512 | 13233 47060 | 4411 12949 784286 60.6 | 16.944 % | c | 718613 | 13233 47060 | 4852 3339 142379 42.6 | 17.064 % | c | 718763 | 13233 47060 | 5337 3489 144681 41.5 | 17.064 % | c | 718990 | 13233 47060 | 5871 3716 148611 40.0 | 17.064 % | c | 719327 | 13233 47060 | 6458 4053 160688 39.6 | 17.064 % | c | 719833 | 13233 47060 | 7103 4559 175624 38.5 | 17.064 % | c | 720594 | 13233 47060 | 7814 5320 205460 38.6 | 17.064 % | c | 721736 | 13233 47060 | 8595 6462 247241 38.3 | 17.064 % | c | 723446 | 13233 47060 | 9455 8172 314461 38.5 | 17.064 % | c | 726010 | 13233 47060 | 10400 5609 177093 31.6 | 17.064 % | c | 729855 | 13233 47060 | 11440 9454 320348 33.9 | 17.064 % | c | 735622 | 13233 47060 | 12585 9147 357511 39.1 | 17.064 % | c | 744271 | 13233 47060 | 13843 11095 382768 34.5 | 17.064 % | c | 757247 | 13233 47060 | 15227 9595 364755 38.0 | 17.064 % | c | 776710 | 13233 47060 | 16750 13144 496887 37.8 | 17.064 % | c | 805903 | 13233 47060 | 18425 16103 650574 40.4 | 17.064 % | c ============================================================================== c [1mFound solution: 37248[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2775 bits: 12/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 836311 | 13236 47071 | 4412 17786 779424 43.8 | 17.064 % | c | 836411 | 13236 47071 | 4853 4547 168356 37.0 | 17.124 % | c | 836561 | 13236 47071 | 5338 4697 172730 36.8 | 17.124 % | c | 836787 | 13236 47071 | 5872 4923 176195 35.8 | 17.124 % | c | 837126 | 13236 47071 | 6459 5262 184655 35.1 | 17.124 % | c | 837632 | 13236 47071 | 7105 5768 201439 34.9 | 17.124 % | c | 838391 | 13236 47071 | 7816 6527 226199 34.7 | 17.124 % | c | 839532 | 13236 47071 | 8597 7668 264608 34.5 | 17.124 % | c | 841240 | 13236 47071 | 9457 9376 352839 37.6 | 17.124 % | c | 843804 | 13236 47071 | 10403 6839 217236 31.8 | 17.124 % | c | 847648 | 13236 47071 | 11443 10683 365217 34.2 | 17.124 % | c | 853416 | 13236 47071 | 12587 10285 433578 42.2 | 17.124 % | c | 862067 | 13236 47071 | 13846 12301 544350 44.3 | 17.124 % | c | 875043 | 13236 47071 | 15231 10795 377613 35.0 | 17.124 % | c | 894505 | 13236 47071 | 16754 14292 546134 38.2 | 17.124 % | c | 923699 | 13236 47071 | 18430 17330 683018 39.4 | 17.124 % | c | 967488 | 13236 47071 | 20273 13061 523270 40.1 | 17.124 % | c | 1033174 | 13236 47071 | 22300 15125 736429 48.7 | 17.124 % | #### 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.98 0.94 2/54 31397 Raw data (stat): 31397 (runsolver) R 31396 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488146011 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99975 s] Raw data (loadavg): 0.93 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1159 0 0 0 995 2 0 0 25 0 1 0 488146011 6377472 1137 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1557 1137 603 41 0 1516 0 vsize: 6228 [startup+20.001 s] Raw data (loadavg): 0.94 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1508 0 0 0 1993 4 0 0 25 0 1 0 488146011 7716864 1486 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1884 1486 603 41 0 1843 0 vsize: 7536 [startup+30.0014 s] Raw data (loadavg): 0.95 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1655 0 0 0 2992 5 0 0 25 0 1 0 488146011 8388608 1633 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2048 1633 603 41 0 2007 0 vsize: 8192 [startup+40.0013 s] Raw data (loadavg): 0.96 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1746 0 0 0 3992 5 0 0 25 0 1 0 488146011 8794112 1724 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1724 603 41 0 2106 0 vsize: 8588 [startup+50.0028 s] Raw data (loadavg): 0.96 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1748 0 0 0 4992 6 0 0 25 0 1 0 488146011 8794112 1726 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1726 603 41 0 2106 0 vsize: 8588 [startup+60.0029 s] Raw data (loadavg): 0.97 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1748 0 0 0 5992 6 0 0 25 0 1 0 488146011 8794112 1726 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1726 603 41 0 2106 0 vsize: 8588 [startup+70.0038 s] Raw data (loadavg): 0.97 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1755 0 0 0 6991 7 0 0 25 0 1 0 488146011 8794112 1733 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1733 603 41 0 2106 0 vsize: 8588 [startup+80.0051 s] Raw data (loadavg): 0.98 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1755 0 0 0 7991 7 0 0 25 0 1 0 488146011 8794112 1733 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1733 603 41 0 2106 0 vsize: 8588 [startup+90.0045 s] Raw data (loadavg): 0.98 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1756 0 0 0 8990 8 0 0 25 0 1 0 488146011 8794112 1734 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1734 603 41 0 2106 0 vsize: 8588 [startup+100.004 s] Raw data (loadavg): 0.98 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1756 0 0 0 9990 8 0 0 25 0 1 0 488146011 8794112 1734 4294967295 134512640 134672761 3221224544 3221223728 134558875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1734 603 41 0 2106 0 vsize: 8588 [startup+110.006 s] Raw data (loadavg): 0.98 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1756 0 0 0 10990 8 0 0 25 0 1 0 488146011 8794112 1734 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1734 603 41 0 2106 0 vsize: 8588 [startup+120.006 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1758 0 0 0 11990 8 0 0 25 0 1 0 488146011 8794112 1736 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2147 1736 603 41 0 2106 0 vsize: 8588 [startup+130.006 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31397 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1772 0 0 0 12990 9 0 0 25 0 1 0 488146011 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2191 1750 603 41 0 2150 0 vsize: 8764 [startup+140.006 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1772 0 0 0 13989 9 0 0 25 0 1 0 488146011 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2191 1750 603 41 0 2150 0 vsize: 8764 [startup+150.006 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1772 0 0 0 14989 9 0 0 25 0 1 0 488146011 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2191 1750 603 41 0 2150 0 vsize: 8764 [startup+160.006 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1772 0 0 0 15989 9 0 0 25 0 1 0 488146011 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2191 1750 603 41 0 2150 0 vsize: 8764 [startup+170.008 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1772 0 0 0 16989 10 0 0 25 0 1 0 488146011 8974336 1750 4294967295 134512640 134672761 3221224544 3221223600 134565076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2191 1750 603 41 0 2150 0 vsize: 8764 [startup+180.008 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1772 0 0 0 17988 10 0 0 25 0 1 0 488146011 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2191 1750 603 41 0 2150 0 vsize: 8764 [startup+190.008 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1772 0 0 0 18988 10 0 0 25 0 1 0 488146011 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2191 1750 603 41 0 2150 0 vsize: 8764 [startup+200.009 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1782 0 0 0 19988 10 0 0 25 0 1 0 488146011 8974336 1760 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2191 1760 603 41 0 2150 0 vsize: 8764 [startup+210.009 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1879 0 0 0 20988 11 0 0 25 0 1 0 488146011 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2291 1857 603 41 0 2250 0 vsize: 9164 [startup+220.009 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1879 0 0 0 21987 12 0 0 25 0 1 0 488146011 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2291 1857 603 41 0 2250 0 vsize: 9164 [startup+230.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1879 0 0 0 22987 12 0 0 25 0 1 0 488146011 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2291 1857 603 41 0 2250 0 vsize: 9164 [startup+240.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1879 0 0 0 23987 12 0 0 25 0 1 0 488146011 9383936 1857 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2291 1857 603 41 0 2250 0 vsize: 9164 [startup+250.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1879 0 0 0 24988 12 0 0 25 0 1 0 488146011 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2291 1857 603 41 0 2250 0 vsize: 9164 [startup+260.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1909 0 0 0 25988 12 0 0 25 0 1 0 488146011 9519104 1887 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2324 1887 603 41 0 2283 0 vsize: 9296 [startup+270.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1950 0 0 0 26988 12 0 0 25 0 1 0 488146011 9674752 1928 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2362 1928 603 41 0 2321 0 vsize: 9448 [startup+280.01 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 1958 0 0 0 27988 12 0 0 25 0 1 0 488146011 9674752 1936 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2362 1936 603 41 0 2321 0 vsize: 9448 [startup+290.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2005 0 0 0 28988 12 0 0 25 0 1 0 488146011 9940992 1983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2427 1983 603 41 0 2386 0 vsize: 9708 [startup+300.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2181 0 0 0 29988 13 0 0 25 0 1 0 488146011 10608640 2159 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2159 603 41 0 2549 0 vsize: 10360 [startup+310.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2181 0 0 0 30988 13 0 0 25 0 1 0 488146011 10608640 2159 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2159 603 41 0 2549 0 vsize: 10360 [startup+320.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2181 0 0 0 31988 13 0 0 25 0 1 0 488146011 10608640 2159 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2159 603 41 0 2549 0 vsize: 10360 [startup+330.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2181 0 0 0 32988 13 0 0 25 0 1 0 488146011 10608640 2159 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2159 603 41 0 2549 0 vsize: 10360 [startup+340.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2181 0 0 0 33988 13 0 0 25 0 1 0 488146011 10608640 2159 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2159 603 41 0 2549 0 vsize: 10360 [startup+350.012 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2183 0 0 0 34988 13 0 0 25 0 1 0 488146011 10608640 2161 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2161 603 41 0 2549 0 vsize: 10360 [startup+360.012 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2183 0 0 0 35988 13 0 0 25 0 1 0 488146011 10608640 2161 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2161 603 41 0 2549 0 vsize: 10360 [startup+370.012 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2183 0 0 0 36988 13 0 0 25 0 1 0 488146011 10608640 2161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2161 603 41 0 2549 0 vsize: 10360 [startup+380.012 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2183 0 0 0 37989 13 0 0 25 0 1 0 488146011 10608640 2161 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2161 603 41 0 2549 0 vsize: 10360 [startup+390.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2183 0 0 0 38989 13 0 0 25 0 1 0 488146011 10608640 2161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2590 2161 603 41 0 2549 0 vsize: 10360 [startup+400.011 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2294 0 0 0 39988 13 0 0 25 0 1 0 488146011 11141120 2272 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2720 2272 603 41 0 2679 0 vsize: 10880 [startup+410.012 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2331 0 0 0 40988 14 0 0 25 0 1 0 488146011 11276288 2309 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2753 2309 603 41 0 2712 0 vsize: 11012 [startup+420.013 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2336 0 0 0 41989 14 0 0 25 0 1 0 488146011 11276288 2314 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2753 2314 603 41 0 2712 0 vsize: 11012 [startup+430.013 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2344 0 0 0 42989 14 0 0 25 0 1 0 488146011 11276288 2322 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2753 2322 603 41 0 2712 0 vsize: 11012 [startup+440.013 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2376 0 0 0 43989 14 0 0 25 0 1 0 488146011 11423744 2354 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2789 2354 603 41 0 2748 0 vsize: 11156 [startup+450.013 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2379 0 0 0 44989 14 0 0 25 0 1 0 488146011 11423744 2357 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2789 2357 603 41 0 2748 0 vsize: 11156 [startup+460.013 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2400 0 0 0 45989 14 0 0 25 0 1 0 488146011 11563008 2378 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2823 2378 603 41 0 2782 0 vsize: 11292 [startup+470.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2400 0 0 0 46989 14 0 0 25 0 1 0 488146011 11563008 2378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2823 2378 603 41 0 2782 0 vsize: 11292 [startup+480.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2403 0 0 0 47990 14 0 0 25 0 1 0 488146011 11563008 2381 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2823 2381 603 41 0 2782 0 vsize: 11292 [startup+490.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2427 0 0 0 48990 14 0 0 25 0 1 0 488146011 11722752 2405 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2862 2405 603 41 0 2821 0 vsize: 11448 [startup+500.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2455 0 0 0 49990 14 0 0 25 0 1 0 488146011 11857920 2433 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2895 2433 603 41 0 2854 0 vsize: 11580 [startup+510.013 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2554 0 0 0 50989 15 0 0 25 0 1 0 488146011 12259328 2532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2993 2532 603 41 0 2952 0 vsize: 11972 [startup+520.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2708 0 0 0 51989 15 0 0 25 0 1 0 488146011 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3125 2686 603 41 0 3084 0 vsize: 12500 [startup+530.015 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2708 0 0 0 52989 15 0 0 25 0 1 0 488146011 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3125 2686 603 41 0 3084 0 vsize: 12500 [startup+540.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2708 0 0 0 53989 15 0 0 25 0 1 0 488146011 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3125 2686 603 41 0 3084 0 vsize: 12500 [startup+550.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2708 0 0 0 54990 15 0 0 25 0 1 0 488146011 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3125 2686 603 41 0 3084 0 vsize: 12500 [startup+560.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2708 0 0 0 55990 15 0 0 25 0 1 0 488146011 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3125 2686 603 41 0 3084 0 vsize: 12500 [startup+570.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2708 0 0 0 56989 15 0 0 25 0 1 0 488146011 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3125 2686 603 41 0 3084 0 vsize: 12500 [startup+580.014 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2708 0 0 0 57989 15 0 0 25 0 1 0 488146011 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3125 2686 603 41 0 3084 0 vsize: 12500 [startup+590.015 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2708 0 0 0 58990 15 0 0 25 0 1 0 488146011 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3125 2686 603 41 0 3084 0 vsize: 12500 [startup+600.015 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2717 0 0 0 59990 15 0 0 25 0 1 0 488146011 12935168 2695 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3158 2695 603 41 0 3117 0 vsize: 12632 [startup+610.015 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2723 0 0 0 60990 15 0 0 25 0 1 0 488146011 12935168 2701 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3158 2701 603 41 0 3117 0 vsize: 12632 [startup+620.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2727 0 0 0 61990 15 0 0 25 0 1 0 488146011 12935168 2705 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3158 2705 603 41 0 3117 0 vsize: 12632 [startup+630.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2733 0 0 0 62990 15 0 0 25 0 1 0 488146011 12935168 2711 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3158 2711 603 41 0 3117 0 vsize: 12632 [startup+640.015 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2737 0 0 0 63990 15 0 0 25 0 1 0 488146011 12935168 2715 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3158 2715 603 41 0 3117 0 vsize: 12632 [startup+650.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2737 0 0 0 64990 15 0 0 25 0 1 0 488146011 12935168 2715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3158 2715 603 41 0 3117 0 vsize: 12632 [startup+660.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2737 0 0 0 65991 15 0 0 25 0 1 0 488146011 12935168 2715 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3158 2715 603 41 0 3117 0 vsize: 12632 [startup+670.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2741 0 0 0 66991 15 0 0 25 0 1 0 488146011 12935168 2719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3158 2719 603 41 0 3117 0 vsize: 12632 [startup+680.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2895 0 0 0 67990 16 0 0 25 0 1 0 488146011 13602816 2873 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3321 2873 603 41 0 3280 0 vsize: 13284 [startup+690.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2902 0 0 0 68990 16 0 0 25 0 1 0 488146011 13602816 2880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3321 2880 603 41 0 3280 0 vsize: 13284 [startup+700.015 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2903 0 0 0 69990 16 0 0 25 0 1 0 488146011 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3321 2881 603 41 0 3280 0 vsize: 13284 [startup+710.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2903 0 0 0 70991 16 0 0 25 0 1 0 488146011 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3321 2881 603 41 0 3280 0 vsize: 13284 [startup+720.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2903 0 0 0 71991 16 0 0 25 0 1 0 488146011 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3321 2881 603 41 0 3280 0 vsize: 13284 [startup+730.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2903 0 0 0 72991 16 0 0 25 0 1 0 488146011 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3321 2881 603 41 0 3280 0 vsize: 13284 [startup+740.016 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2903 0 0 0 73991 16 0 0 25 0 1 0 488146011 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3321 2881 603 41 0 3280 0 vsize: 13284 [startup+750.017 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2903 0 0 0 74991 16 0 0 25 0 1 0 488146011 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3321 2881 603 41 0 3280 0 vsize: 13284 [startup+760.023 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 75992 16 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223544 1075349791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+770.024 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 76992 16 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+780.024 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 77992 16 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+790.024 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 78992 16 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223680 134565098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+800.025 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 79993 16 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+810.025 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 80993 16 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+820.024 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 81993 17 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+830.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 82993 17 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+840.025 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 83993 17 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+850.025 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 84993 17 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+860.025 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 85994 17 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+870.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 86994 17 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+880.025 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2930 0 0 0 87994 17 0 0 25 0 1 0 488146011 13733888 2908 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2908 603 41 0 3312 0 vsize: 13412 [startup+890.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 88994 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+900.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 89994 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+910.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 90994 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+920.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 91994 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+930.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 92994 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+940.025 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 93994 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+950.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 94995 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+960.026 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 95995 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+970.027 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 96995 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+980.027 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 97995 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+990.027 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 98995 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+1000.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 2939 0 0 0 99995 17 0 0 25 0 1 0 488146011 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3353 2917 603 41 0 3312 0 vsize: 13412 [startup+1010.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3004 0 0 0 100996 17 0 0 25 0 1 0 488146011 14004224 2982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3419 2982 603 41 0 3378 0 vsize: 13676 [startup+1020.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3042 0 0 0 101995 17 0 0 25 0 1 0 488146011 14274560 3020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3485 3020 603 41 0 3444 0 vsize: 13940 [startup+1030.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3077 0 0 0 102995 18 0 0 25 0 1 0 488146011 14405632 3055 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3517 3055 603 41 0 3476 0 vsize: 14068 [startup+1040.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3080 0 0 0 103996 18 0 0 25 0 1 0 488146011 14405632 3058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3517 3058 603 41 0 3476 0 vsize: 14068 [startup+1050.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3165 0 0 0 104995 18 0 0 25 0 1 0 488146011 14671872 3143 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3582 3143 603 41 0 3541 0 vsize: 14328 [startup+1060.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3165 0 0 0 105995 18 0 0 25 0 1 0 488146011 14671872 3143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3582 3143 603 41 0 3541 0 vsize: 14328 [startup+1070.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3393 0 0 0 106995 19 0 0 25 0 1 0 488146011 15601664 3371 4294967295 134512640 134672761 3221224544 3221223712 134561086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3809 3371 603 41 0 3768 0 vsize: 15236 [startup+1080.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3397 0 0 0 107995 19 0 0 25 0 1 0 488146011 15601664 3375 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3809 3375 603 41 0 3768 0 vsize: 15236 [startup+1090.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3477 0 0 0 108995 19 0 0 25 0 1 0 488146011 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3455 603 41 0 3869 0 vsize: 15640 [startup+1100.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3477 0 0 0 109995 19 0 0 25 0 1 0 488146011 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3455 603 41 0 3869 0 vsize: 15640 [startup+1110.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3477 0 0 0 110996 19 0 0 25 0 1 0 488146011 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3455 603 41 0 3869 0 vsize: 15640 [startup+1120.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3477 0 0 0 111996 19 0 0 25 0 1 0 488146011 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3455 603 41 0 3869 0 vsize: 15640 [startup+1130.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3477 0 0 0 112996 19 0 0 25 0 1 0 488146011 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3455 603 41 0 3869 0 vsize: 15640 [startup+1140.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3477 0 0 0 113996 19 0 0 25 0 1 0 488146011 16015360 3455 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3455 603 41 0 3869 0 vsize: 15640 [startup+1150.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3477 0 0 0 114996 19 0 0 25 0 1 0 488146011 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3455 603 41 0 3869 0 vsize: 15640 [startup+1160.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3479 0 0 0 115996 19 0 0 25 0 1 0 488146011 16015360 3457 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3457 603 41 0 3869 0 vsize: 15640 [startup+1170.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3479 0 0 0 116997 19 0 0 25 0 1 0 488146011 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3457 603 41 0 3869 0 vsize: 15640 [startup+1180.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3479 0 0 0 117997 19 0 0 25 0 1 0 488146011 16015360 3457 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3457 603 41 0 3869 0 vsize: 15640 [startup+1190.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3479 0 0 0 118997 19 0 0 25 0 1 0 488146011 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3457 603 41 0 3869 0 vsize: 15640 [startup+1200.03 s] Raw data (loadavg): 0.99 0.98 0.94 2/54 31399 Raw data (stat): 31397 (minisat+) R 31396 25285 25284 0 -1 0 3479 0 0 0 119997 19 0 0 25 0 1 0 488146011 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3910 3457 603 41 0 3869 0 vsize: 15640 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.04 s] Raw data (loadavg): 0.99 0.98 0.94 1/54 31399 Raw data (stat): 31397 (minisat+) Z 31396 25285 25284 0 -1 12 3482 0 0 0 119997 20 0 0 25 0 1 0 488146011 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.04 CPU time (s): 1200.18 CPU user time (s): 1199.98 CPU system time (s): 0.201969 CPU usage (%): 100.012 Max. virtual memory (Kb): 15640 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####