Name | mps-v2-20-10/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-20-10-maros.opb |
MD5SUM | df23206734a7a5ecc1a5d03632e7fa81 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 344750 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 90 |
Biggest coefficient in the objective function | 4831838208 |
Number of bits for the biggest coefficient in the objective function | 33 |
Sum of the numbers in the objective function | 15032909794 |
Number of bits of the sum of numbers in the objective function | 34 |
Biggest number in a constraint | 4831838208 |
Number of bits of the biggest number in a constraint | 33 |
Biggest sum of numbers in a constraint | 15032909794 |
Number of bits of the biggest sum of numbers | 34 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 30.9553 |
Number of variables | 90 |
Total number of constraints | 6 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 15 |
Maximum length of a constraint | 90 |
LAUNCH ON wulflinc21 THE 2005-09-20 02:26:49 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3127 boxname=wulflinc21 idbench=783 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: df23206734a7a5ecc1a5d03632e7fa81 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-maros.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-maros.opb IDLAUNCH: 3127 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 840356 kB Buffers: 30952 kB Cached: 133636 kB SwapCached: 788 kB Active: 50088 kB Inactive: 117004 kB HighTotal: 131008 kB HighFree: 24108 kB LowTotal: 903652 kB LowFree: 816248 kB SwapTotal: 2097892 kB SwapFree: 2096456 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 21572 kB Committed_AS: 64368 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:27:21 (client local time) WITH STATUS 30 IN 30.9553 SECONDS stats: 3127 0 30.9553 30
c Parsing PB file... c Converting 6 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): s c ---[ 5]---> BDD-cost: 14 c ---[ 3]---> Sorter-cost: 1222 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 521 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 1]---> Sorter-cost: 546 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 5697 13365 | 1899 0 0 nan | 0.000 % | c | 102 | 5697 13365 | 2088 102 2002 19.6 | 1.781 % | c ============================================================================== c [1mFound solution: 423991[0m c ---[ 0]---> Sorter-cost: 1242 Base: 2 2 2 2 2 2 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 | 151 | 8635 20227 | 2878 151 2317 15.3 | 1.781 % | c ============================================================================== c [1mFound solution: 420608[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 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 | 167 | 8677 20361 | 2892 167 2472 14.8 | 1.781 % | c ============================================================================== c [1mFound solution: 391113[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 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 | 198 | 8689 20396 | 2896 198 2965 15.0 | 1.781 % | c | 298 | 8689 20396 | 3185 298 3751 12.6 | 1.263 % | c ============================================================================== c [1mFound solution: 384569[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 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 | 308 | 8706 20438 | 2902 308 3907 12.7 | 1.263 % | c | 408 | 8706 20438 | 3192 408 5000 12.3 | 1.290 % | c | 559 | 8706 20438 | 3511 559 7666 13.7 | 1.290 % | c ============================================================================== c [1mFound solution: 383973[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 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 | 710 | 8723 20477 | 2907 710 9537 13.4 | 1.290 % | c | 810 | 8723 20477 | 3197 810 10487 12.9 | 1.319 % | c ============================================================================== c [1mFound solution: 370341[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 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 | 922 | 8741 20519 | 2913 922 12814 13.9 | 1.319 % | c | 1023 | 8741 20519 | 3204 1023 14426 14.1 | 1.347 % | c ============================================================================== c [1mFound solution: 359039[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 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 | 1069 | 8758 20565 | 2919 1069 14863 13.9 | 1.347 % | c | 1169 | 8758 20565 | 3210 1169 16648 14.2 | 1.374 % | c | 1319 | 8758 20565 | 3531 1319 18753 14.2 | 1.374 % | c | 1544 | 8758 20565 | 3885 1544 21347 13.8 | 1.374 % | c | 1882 | 8758 20565 | 4273 1882 25220 13.4 | 1.374 % | c | 2391 | 8758 20565 | 4701 2391 32011 13.4 | 1.374 % | c ============================================================================== c [1mFound solution: 352165[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 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 | 2781 | 8765 20587 | 2921 2781 39871 14.3 | 1.374 % | c | 2882 | 8765 20587 | 3213 2882 41280 14.3 | 1.403 % | c | 3035 | 8765 20587 | 3534 3035 43433 14.3 | 1.403 % | c | 3261 | 8765 20587 | 3887 3261 48979 15.0 | 1.403 % | c | 3598 | 8765 20587 | 4276 3598 54378 15.1 | 1.403 % | c | 4106 | 8765 20587 | 4704 4106 64249 15.6 | 1.403 % | c ============================================================================== c [1mFound solution: 351712[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 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 | 4333 | 8775 20617 | 2925 4333 67578 15.6 | 1.403 % | c | 4434 | 8775 20617 | 3217 2268 34255 15.1 | 1.431 % | c | 4585 | 8775 20617 | 3539 2419 36143 14.9 | 1.431 % | c | 4810 | 8775 20617 | 3893 2644 38975 14.7 | 1.431 % | c ============================================================================== c [1mFound solution: 351204[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 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 | 5031 | 8791 20655 | 2930 2865 43803 15.3 | 1.431 % | c | 5131 | 8791 20655 | 3223 2965 45101 15.2 | 1.459 % | c | 5282 | 8791 20655 | 3545 3116 46766 15.0 | 1.459 % | c ============================================================================== c [1mFound solution: 351203[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 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 | 5491 | 8798 20674 | 2932 3325 49903 15.0 | 1.459 % | c | 5594 | 8798 20674 | 3225 1766 21211 12.0 | 1.488 % | c | 5746 | 8798 20674 | 3547 1918 23871 12.4 | 1.488 % | c | 5972 | 8798 20674 | 3902 2144 27610 12.9 | 1.488 % | c | 6309 | 8798 20674 | 4292 2481 33375 13.5 | 1.488 % | c ============================================================================== c [1mFound solution: 350714[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 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 | 6448 | 8819 20725 | 2939 2620 35479 13.5 | 1.488 % | c | 6550 | 8819 20725 | 3232 2722 37924 13.9 | 1.513 % | c | 6700 | 8819 20725 | 3556 2872 40741 14.2 | 1.513 % | c | 6925 | 8819 20725 | 3911 3097 44519 14.4 | 1.513 % | c | 7262 | 8819 20725 | 4302 3434 50652 14.8 | 1.513 % | c ============================================================================== c [1mFound solution: 350066[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 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 | 7445 | 8834 20764 | 2944 3617 53698 14.8 | 1.513 % | c | 7546 | 8834 20764 | 3238 1910 23165 12.1 | 1.540 % | c | 7700 | 8834 20764 | 3562 2064 24536 11.9 | 1.540 % | c | 7925 | 8834 20764 | 3918 2289 29408 12.8 | 1.540 % | c | 8262 | 8834 20764 | 4310 2626 35596 13.6 | 1.540 % | c | 8768 | 8834 20764 | 4741 3132 44465 14.2 | 1.540 % | c | 9527 | 8834 20764 | 5215 3891 56817 14.6 | 1.540 % | c ============================================================================== c [1mFound solution: 348198[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 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 | 9708 | 8854 20810 | 2951 4072 60279 14.8 | 1.540 % | c | 9808 | 8854 20810 | 3246 2136 24643 11.5 | 1.566 % | c | 9961 | 8854 20810 | 3570 2289 26558 11.6 | 1.567 % | c | 10186 | 8854 20810 | 3927 2514 31320 12.5 | 1.567 % | c | 10525 | 8854 20810 | 4320 2853 37361 13.1 | 1.567 % | c | 11031 | 8854 20810 | 4752 3359 45443 13.5 | 1.566 % | c ============================================================================== c [1mFound solution: 348151[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 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 | 11515 | 8868 20842 | 2956 3843 54113 14.1 | 1.566 % | c | 11617 | 8868 20842 | 3251 2024 22531 11.1 | 1.594 % | c | 11767 | 8868 20842 | 3576 2174 24167 11.1 | 1.594 % | c | 11993 | 8868 20842 | 3934 2400 26755 11.1 | 1.594 % | c | 12330 | 8868 20842 | 4327 2737 31077 11.4 | 1.595 % | c | 12836 | 8868 20842 | 4760 3243 42263 13.0 | 1.594 % | c ============================================================================== c [1mFound solution: 348139[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 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 | 13046 | 8884 20878 | 2961 3453 45788 13.3 | 1.594 % | c | 13148 | 8884 20878 | 3257 1829 21584 11.8 | 1.622 % | c | 13298 | 8884 20878 | 3582 1979 23723 12.0 | 1.622 % | c ============================================================================== c [1mFound solution: 348133[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 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 | 13351 | 8894 20902 | 2964 2032 24568 12.1 | 1.622 % | c | 13451 | 8894 20902 | 3260 2132 26507 12.4 | 1.650 % | c | 13602 | 8894 20902 | 3586 2283 29085 12.7 | 1.650 % | c | 13827 | 8894 20902 | 3945 2508 34003 13.6 | 1.649 % | c ============================================================================== c [1mFound solution: 348128[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 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 | 13899 | 8902 20924 | 2967 2580 35575 13.8 | 1.649 % | c ============================================================================== c [1mFound solution: 348117[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 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 | 13988 | 8913 20957 | 2971 2669 37250 14.0 | 1.649 % | c | 14088 | 8913 20957 | 3268 2769 39246 14.2 | 1.705 % | c | 14238 | 8913 20957 | 3594 2919 41757 14.3 | 1.705 % | c ============================================================================== c [1mFound solution: 348069[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 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 | 14396 | 8921 20980 | 2973 3077 43578 14.2 | 1.705 % | c | 14496 | 8921 20980 | 3270 1639 16821 10.3 | 1.733 % | c ============================================================================== c [1mFound solution: 346080[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 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 | 14585 | 8930 21003 | 2976 1728 17989 10.4 | 1.733 % | c | 14685 | 8930 21003 | 3273 1828 19860 10.9 | 1.761 % | c | 14835 | 8930 21003 | 3600 1978 22834 11.5 | 1.760 % | c | 15060 | 8930 21003 | 3961 2203 27004 12.3 | 1.760 % | c | 15402 | 8930 21003 | 4357 2545 33751 13.3 | 1.760 % | c | 15909 | 8930 21003 | 4792 3052 42187 13.8 | 1.760 % | c ============================================================================== c [1mFound solution: 346053[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 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 | 16247 | 8941 21034 | 2980 3390 47407 14.0 | 1.760 % | c ============================================================================== c [1mFound solution: 345541[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 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 | 16253 | 8953 21066 | 2984 1701 17861 10.5 | 1.760 % | c | 16353 | 8953 21066 | 3282 1801 19982 11.1 | 1.814 % | c | 16503 | 8953 21066 | 3610 1951 23189 11.9 | 1.815 % | c | 16728 | 8953 21066 | 3971 2176 27434 12.6 | 1.814 % | c | 17065 | 8953 21066 | 4368 2513 34906 13.9 | 1.814 % | c | 17571 | 8953 21066 | 4805 3019 46530 15.4 | 1.814 % | c | 18330 | 8953 21066 | 5286 3778 58445 15.5 | 1.814 % | c ============================================================================== c [1mFound solution: 345540[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 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 | 19242 | 8969 21106 | 2989 4690 83910 17.9 | 1.814 % | c | 19342 | 8969 21106 | 3287 2445 39645 16.2 | 1.840 % | c | 19492 | 8969 21106 | 3616 2595 42083 16.2 | 1.840 % | c | 19718 | 8969 21106 | 3978 2821 47313 16.8 | 1.840 % | c | 20055 | 8855 20853 | 4376 2816 47124 16.7 | 2.774 % | c | 20561 | 8855 20853 | 4813 3322 56187 16.9 | 2.775 % | c | 21323 | 8855 20853 | 5295 4084 68726 16.8 | 2.775 % | c | 22462 | 8855 20853 | 5824 5223 92349 17.7 | 2.774 % | c ============================================================================== c [1mFound solution: 345157[0m c ---[ 0]---> Sorter-cost: 270 Base: 2 2 2 2 2 2 2 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 | 22548 | 9477 22302 | 3159 5309 94646 17.8 | 2.774 % | c | 22648 | 9477 22302 | 3474 2755 37055 13.5 | 2.628 % | c | 22799 | 9477 22302 | 3822 2906 39665 13.6 | 2.628 % | c | 23025 | 9477 22302 | 4204 3132 44507 14.2 | 2.628 % | c | 23363 | 9477 22302 | 4625 3470 49689 14.3 | 2.628 % | c | 23869 | 9477 22302 | 5087 3976 60472 15.2 | 2.628 % | c ============================================================================== c [1mFound solution: 345059[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 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 | 24518 | 9488 22329 | 3162 4625 72381 15.6 | 2.628 % | c | 24619 | 9488 22329 | 3478 2414 29648 12.3 | 2.652 % | c | 24770 | 9488 22329 | 3826 2565 32022 12.5 | 2.653 % | c | 24996 | 9488 22329 | 4208 2791 37442 13.4 | 2.652 % | c | 25335 | 9488 22329 | 4629 3130 45295 14.5 | 2.653 % | c | 25841 | 9488 22329 | 5092 3636 56557 15.6 | 2.652 % | c ============================================================================== c [1mFound solution: 345056[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 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 | 26354 | 9365 22054 | 3121 3892 66095 17.0 | 2.652 % | c | 26456 | 9365 22054 | 3433 2048 26720 13.0 | 3.748 % | c ============================================================================== c [1mFound solution: 345018[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 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 | 26573 | 9379 22088 | 3126 2165 28757 13.3 | 3.748 % | c | 26673 | 9379 22088 | 3438 2265 31041 13.7 | 3.770 % | c | 26823 | 9379 22088 | 3782 2415 32970 13.7 | 3.769 % | c | 27048 | 9379 22088 | 4160 2640 38793 14.7 | 3.769 % | c ============================================================================== c [1mFound solution: 345016[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 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 | 27338 | 9397 22132 | 3132 2930 43585 14.9 | 3.769 % | c | 27439 | 9397 22132 | 3445 3031 46113 15.2 | 3.789 % | c ============================================================================== c [1mFound solution: 345014[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 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 | 27499 | 9415 22175 | 3138 3091 46938 15.2 | 3.789 % | c | 27599 | 9415 22175 | 3451 3191 49763 15.6 | 3.808 % | c | 27750 | 9415 22175 | 3796 3342 52550 15.7 | 3.808 % | c | 27976 | 9415 22175 | 4176 3568 57763 16.2 | 3.808 % | c | 28313 | 9415 22175 | 4594 3905 65556 16.8 | 3.808 % | c ============================================================================== c [1mFound solution: 344850[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 28447 | 9433 22216 | 3144 4039 68103 16.9 | 3.808 % | c | 28552 | 9433 22216 | 3458 2125 26155 12.3 | 3.827 % | c | 28702 | 9433 22216 | 3804 2275 29161 12.8 | 3.827 % | c | 28927 | 9433 22216 | 4184 2500 32831 13.1 | 3.827 % | c | 29264 | 9433 22216 | 4603 2837 40707 14.3 | 3.827 % | c ============================================================================== c [1mFound solution: 344846[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 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 | 29426 | 9454 22264 | 3151 2999 44667 14.9 | 3.827 % | c | 29527 | 9454 22264 | 3466 3100 47222 15.2 | 3.844 % | c | 29678 | 9454 22264 | 3812 3251 49584 15.3 | 3.844 % | c | 29904 | 9269 21851 | 4193 3221 49634 15.4 | 5.209 % | c | 30241 | 9269 21851 | 4613 3558 57893 16.3 | 5.209 % | c | 30747 | 9269 21851 | 5074 4064 67694 16.7 | 5.209 % | c ============================================================================== c [1mFound solution: 344827[0m c ---[ 0]---> Sorter-cost: 467 Base: 2 2 2 2 2 2 2 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 | 31182 | 10405 24498 | 3468 4499 75323 16.7 | 5.209 % | c | 31288 | 10405 24498 | 3814 2356 25757 10.9 | 4.714 % | c | 31440 | 10405 24498 | 4196 2508 29351 11.7 | 4.714 % | c | 31665 | 10405 24498 | 4615 2733 35741 13.1 | 4.714 % | c | 32003 | 10405 24498 | 5077 3071 45403 14.8 | 4.714 % | c | 32509 | 10405 24498 | 5585 3577 59333 16.6 | 4.714 % | c | 33269 | 10405 24498 | 6143 4337 76014 17.5 | 4.714 % | c ============================================================================== c [1mFound solution: 344826[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 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 | 33513 | 10421 24537 | 3473 4581 80851 17.6 | 4.714 % | c | 33614 | 10421 24537 | 3820 2392 30228 12.6 | 4.731 % | c | 33765 | 10421 24537 | 4202 2543 34190 13.4 | 4.731 % | c | 33991 | 10421 24537 | 4622 2769 39429 14.2 | 4.731 % | c | 34328 | 10421 24537 | 5084 3106 48004 15.5 | 4.731 % | c | 34834 | 10421 24537 | 5593 3612 56272 15.6 | 4.731 % | c | 35593 | 10421 24537 | 6152 4371 71560 16.4 | 4.731 % | c ============================================================================== c [1mFound solution: 344820[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 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 | 36257 | 10441 24582 | 3480 5035 87050 17.3 | 4.731 % | c ============================================================================== c [1mFound solution: 344818[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 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 | 36289 | 10455 24614 | 3485 2550 32881 12.9 | 4.731 % | c | 36390 | 10455 24614 | 3833 2651 35561 13.4 | 4.764 % | c | 36540 | 10455 24614 | 4216 2801 40258 14.4 | 4.764 % | c ============================================================================== c [1mFound solution: 344816[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 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 | 36615 | 10473 24655 | 3491 2876 41424 14.4 | 4.764 % | c | 36719 | 10473 24655 | 3840 2980 43256 14.5 | 4.781 % | c | 36869 | 10473 24655 | 4224 3130 46685 14.9 | 4.781 % | c | 37095 | 10473 24655 | 4646 3356 50303 15.0 | 4.781 % | c | 37432 | 10473 24655 | 5111 3693 57298 15.5 | 4.781 % | c | 37938 | 10473 24655 | 5622 4199 68810 16.4 | 4.781 % | c ============================================================================== c [1mFound solution: 344799[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 38280 | 10488 24691 | 3496 4541 74852 16.5 | 4.781 % | c | 38380 | 10488 24691 | 3845 2371 27110 11.4 | 4.798 % | c | 38532 | 10488 24691 | 4230 2523 30322 12.0 | 4.798 % | c | 38757 | 10488 24691 | 4653 2748 35294 12.8 | 4.798 % | c ============================================================================== c [1mFound solution: 344796[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 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 | 38938 | 10505 24733 | 3501 2929 38257 13.1 | 4.798 % | c | 39040 | 10505 24733 | 3851 3031 40750 13.4 | 4.813 % | c | 39190 | 10505 24733 | 4236 3181 44416 14.0 | 4.813 % | c | 39416 | 10505 24733 | 4659 3407 46941 13.8 | 4.813 % | c | 39754 | 10505 24733 | 5125 3745 51360 13.7 | 4.813 % | c | 40260 | 10505 24733 | 5638 4251 60495 14.2 | 4.813 % | c ============================================================================== c [1mFound solution: 344793[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 40364 | 10520 24769 | 3506 4355 62857 14.4 | 4.813 % | c | 40464 | 10520 24769 | 3856 2278 23960 10.5 | 4.829 % | c | 40614 | 10520 24769 | 4242 2428 26268 10.8 | 4.829 % | c | 40839 | 10520 24769 | 4666 2653 31485 11.9 | 4.829 % | c ============================================================================== c [1mFound solution: 344792[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 41084 | 10535 24805 | 3511 2898 35953 12.4 | 4.829 % | c | 41185 | 10535 24805 | 3862 2999 37393 12.5 | 4.846 % | c | 41336 | 10535 24805 | 4248 3150 40973 13.0 | 4.846 % | c | 41561 | 10535 24805 | 4673 3375 44849 13.3 | 4.846 % | c ============================================================================== c [1mFound solution: 344789[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 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 | 41611 | 10550 24842 | 3516 3425 45810 13.4 | 4.846 % | c ============================================================================== c [1mFound solution: 344788[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 41628 | 10565 24878 | 3521 3442 46084 13.4 | 4.846 % | c ============================================================================== c [1mFound solution: 344786[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 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 | 41657 | 10580 24913 | 3526 3471 46615 13.4 | 4.846 % | c | 41757 | 10580 24913 | 3878 3571 48575 13.6 | 4.894 % | c ============================================================================== c [1mFound solution: 344785[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 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 | 41833 | 10598 24956 | 3532 3647 49771 13.6 | 4.894 % | c | 41933 | 10598 24956 | 3885 3747 51741 13.8 | 4.908 % | c | 42085 | 10598 24956 | 4273 3899 54367 13.9 | 4.908 % | c | 42310 | 10598 24956 | 4701 4124 57579 14.0 | 4.908 % | c ============================================================================== c [1mFound solution: 344784[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 42465 | 10615 24996 | 3538 4279 59647 13.9 | 4.908 % | c | 42566 | 10615 24996 | 3891 2241 21409 9.6 | 4.923 % | c | 42716 | 10615 24996 | 4280 2391 24371 10.2 | 4.923 % | c | 42941 | 10615 24996 | 4709 2616 28310 10.8 | 4.923 % | c | 43278 | 10615 24996 | 5179 2953 36099 12.2 | 4.923 % | c ============================================================================== c [1mFound solution: 344783[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 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 | 43458 | 10633 25039 | 3544 3133 39095 12.5 | 4.923 % | c | 43561 | 10633 25039 | 3898 3236 40821 12.6 | 4.936 % | c | 43713 | 10633 25039 | 4288 3388 43520 12.8 | 4.937 % | c ============================================================================== c [1mFound solution: 344781[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 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 | 43721 | 10653 25086 | 3551 3396 43617 12.8 | 4.937 % | c ============================================================================== c [1mFound solution: 344779[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 43726 | 10670 25126 | 3556 3401 43693 12.8 | 4.937 % | c ============================================================================== c [1mFound solution: 344775[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 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 | 43737 | 10687 25166 | 3562 3412 43874 12.9 | 4.937 % | c ============================================================================== c [1mFound solution: 344774[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 43807 | 10704 25206 | 3568 3482 46407 13.3 | 4.937 % | c | 43909 | 10704 25206 | 3924 3584 48204 13.4 | 4.993 % | c ============================================================================== c [1mFound solution: 344771[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 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 | 43950 | 10719 25241 | 3573 3625 48855 13.5 | 4.993 % | c | 44050 | 10719 25241 | 3930 3725 50529 13.6 | 5.009 % | c | 44200 | 10719 25241 | 4323 3875 53661 13.8 | 5.009 % | c ============================================================================== c [1mFound solution: 344766[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 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 | 44222 | 10737 25283 | 3579 3897 54491 14.0 | 5.009 % | c ============================================================================== c [1mFound solution: 344765[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 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 | 44252 | 10755 25325 | 3585 1979 19086 9.6 | 5.009 % | c | 44352 | 10755 25325 | 3943 2079 20662 9.9 | 5.035 % | c | 44503 | 10755 25325 | 4337 2230 23422 10.5 | 5.035 % | c | 44729 | 10755 25325 | 4771 2456 27555 11.2 | 5.035 % | c ============================================================================== c [1mFound solution: 344764[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 44918 | 10773 25368 | 3591 2645 31294 11.8 | 5.035 % | c | 45018 | 10773 25368 | 3950 2745 33066 12.0 | 5.048 % | c ============================================================================== c [1mFound solution: 344763[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 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 | 45041 | 10790 25407 | 3596 2768 33482 12.1 | 5.048 % | c ============================================================================== c [1mFound solution: 344757[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 45055 | 10808 25449 | 3602 2782 33894 12.2 | 5.048 % | c | 45158 | 10808 25449 | 3962 2885 35341 12.2 | 5.076 % | c ============================================================================== c [1mFound solution: 344756[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 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 | 45188 | 10825 25488 | 3608 2915 35978 12.3 | 5.076 % | c ============================================================================== c [1mFound solution: 344755[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 45263 | 10842 25527 | 3614 2990 36745 12.3 | 5.076 % | c ============================================================================== c [1mFound solution: 344754[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 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 | 45271 | 10859 25566 | 3619 2998 36997 12.3 | 5.076 % | c | 45372 | 10859 25566 | 3980 3099 38253 12.3 | 5.118 % | c | 45522 | 10859 25566 | 4378 3249 40622 12.5 | 5.118 % | c ============================================================================== c [1mFound solution: 344752[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 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 | 45701 | 10876 25605 | 3625 3428 44183 12.9 | 5.118 % | c | 45801 | 10876 25605 | 3987 3528 45577 12.9 | 5.132 % | c | 45951 | 10876 25605 | 4386 3678 47750 13.0 | 5.132 % | c ============================================================================== c [1mFound solution: 344751[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 45959 | 10893 25644 | 3631 3686 47880 13.0 | 5.132 % | c | 46059 | 10893 25644 | 3994 3786 49618 13.1 | 5.146 % | c ============================================================================== c [1mFound solution: 344750[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 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 | 46153 | 10910 25683 | 3636 3880 51517 13.3 | 5.146 % | c | 46253 | 10910 25683 | 3999 2040 18747 9.2 | 5.160 % | c | 46403 | 10910 25683 | 4399 2190 21504 9.8 | 5.160 % | c | 46628 | 10585 24949 | 4839 1499 9418 6.3 | 7.195 % | c ============================================================================== c [1mOptimal solution: 344750[0m s OPTIMUM FOUND v VOL1_bit_10 -VOL1_bit_9 VOL1_bit_8 -VOL1_bit_7 VOL1_bit_6 -VOL1_bit_5 VOL1_bit_4 -VOL1_bit_3 VOL1_bit_2 -VOL1_bit_1 VOL1_bit0 VOL1_bit1 -VOL1_bit2 -VOL1_bit3 -VOL1_bit4 -VOL1_bit5 -VOL1_bit6 -VOL1_bit7 -VOL1_bit8 -VOL1_bit9 -VOL1_bit10 -VOL1_bit11 -VOL1_bit12 -VOL1_bit13 -VOL1_bit14 -VOL1_bit15 -VOL1_bit16 -VOL1_bit17 -VOL1_bit18 -VOL1_bit19 VOL2_bit_10 -VOL2_bit_9 VOL2_bit_8 -VOL2_bit_7 VOL2_bit_6 -VOL2_bit_5 VOL2_bit_4 -VOL2_bit_3 VOL2_bit_2 -VOL2_bit_1 VOL2_bit0 -VOL2_bit1 VOL2_bit2 VOL2_bit3 -VOL2_bit4 -VOL2_bit5 -VOL2_bit6 -VOL2_bit7 -VOL2_bit8 -VOL2_bit9 -VOL2_bit10 -VOL2_bit11 -VOL2_bit12 -VOL2_bit13 -VOL2_bit14 -VOL2_bit15 -VOL2_bit16 -VOL2_bit17 -VOL2_bit18 -VOL2_bit19 -VOL3_bit_10 -VOL3_bit_9 -VOL3_bit_8 -VOL3_bit_7 -VOL3_bit_6 -VOL3_bit_5 -VOL3_bit_4 -VOL3_bit_3 -VOL3_bit_2 -VOL3_bit_1 -VOL3_bit0 VOL3_bit1 VOL3_bit2 VOL3_bit3 VOL3_bit4 VOL4_bit_10 -VOL4_bit_9 -VOL4_bit_8 -VOL4_bit_7 -VOL4_bit_6 -VOL4_bit_5 -VOL4_bit_4 -VOL4_bit_3 -VOL4_bit_2 -VOL4_bit_1 -VOL4_bit0 -VOL4_bit1 -VOL4_bit2 -VOL4_bit3 -VOL4_bit4 c _______________________________________________________________________________ c c restarts : 222 c conflicts : 46726 (1513 /sec) c decisions : 78990 (2558 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 30.8763 s c _______________________________________________________________________________
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/12421/stat): 12421 (minisat+_script) R 12420 12421 20602 0 -1 0 19 0 0 0 0 0 0 0 24 0 1 0 1732198193 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/12421/statm): 174 9 169 147 0 27 0 [pid=12421] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=12422 New process pid=12423 New process pid=12424 execve syscall for /bin/sed executable One traced child (pid=12423) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=12424) exited with status: 0 One traced child (pid=12422) exited with status: 0 New process pid=12425 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-maros.opb [startup+10.0029 s] Raw data (loadavg): 0.93 0.96 0.91 2/58 12425 Raw data (/proc/12421/stat): 12421 (minisat+_script) S 12420 12421 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732198193 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12421/statm): 531 226 485 147 0 384 0 [pid=12421] vsize: 2124 Raw data (/proc/12425/stat): 12425 (minisat+_64-bit) R 12421 12421 20602 0 -1 0 556 0 0 0 989 2 0 0 25 0 1 0 1732198198 2646016 543 4294967295 134512640 135094434 3221224432 3221223024 134551421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12425/statm): 646 543 145 145 0 501 0 [pid=12425] vsize: 2584 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 4708 [startup+20.0036 s] Raw data (loadavg): 0.94 0.96 0.91 2/58 12425 Raw data (/proc/12421/stat): 12421 (minisat+_script) S 12420 12421 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732198193 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12421/statm): 531 226 485 147 0 384 0 [pid=12421] vsize: 2124 Raw data (/proc/12425/stat): 12425 (minisat+_64-bit) R 12421 12421 20602 0 -1 0 624 0 0 0 1987 3 0 0 25 0 1 0 1732198198 2916352 611 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12425/statm): 712 611 145 145 0 567 0 [pid=12425] vsize: 2848 Current children cumulated CPU time (s) 19.9 Current children cumulated vsize (Kb) 4972 [startup+30.0053 s] Raw data (loadavg): 0.95 0.96 0.91 2/58 12425 Raw data (/proc/12421/stat): 12421 (minisat+_script) S 12420 12421 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732198193 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12421/statm): 531 226 485 147 0 384 0 [pid=12421] vsize: 2124 Raw data (/proc/12425/stat): 12425 (minisat+_64-bit) R 12421 12421 20602 0 -1 0 696 0 0 0 2985 4 0 0 25 0 1 0 1732198198 3350528 683 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12425/statm): 818 683 145 145 0 673 0 [pid=12425] vsize: 3272 Current children cumulated CPU time (s) 29.89 Current children cumulated vsize (Kb) 5396 One traced child (pid=12425) exited with status: 30 One traced child (pid=12421) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 31.0414 CPU time (s): 30.9553 CPU user time (s): 30.8833 CPU system time (s): 0.071989 CPU usage (%): 99.7225 Max. virtual memory (cumulated for all children) (Kb): 5396
Verifier: OK 344750