Name | normalized-opb/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 | NO |
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 | SAT |
Best CPU time to get the best result obtained on this benchmark | 29.6805 |
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 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc17 THE 2005-05-25 21:18:14 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22367 boxname=wulflinc17 idbench=1183 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: df23206734a7a5ecc1a5d03632e7fa81 /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-maros.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-maros.opb IDLAUNCH: 22367 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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 : 3 cpu MHz : 451.072 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: 888836 kB Buffers: 22776 kB Cached: 100976 kB SwapCached: 484 kB Active: 18300 kB Inactive: 107508 kB HighTotal: 131008 kB HighFree: 29344 kB LowTotal: 903652 kB LowFree: 859492 kB SwapTotal: 2097892 kB SwapFree: 2096560 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5276 kB Slab: 14348 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 21:18:45 (client local time) WITH STATUS 30 IN 30.3834 SECONDS stats: 22367 0 30.3834 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 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 (1541 /sec) c decisions : 78990 (2605 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 30.3224 s c _______________________________________________________________________________ #### 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.97 0.91 2/54 27034 Raw data (stat): 27034 (runsolver) R 27033 7475 7474 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842071962 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 0.93 0.97 0.91 2/55 27038 Raw data (stat): 27034 (minisat+_script) S 27033 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842071962 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0076 s] Raw data (loadavg): 0.94 0.97 0.91 2/55 27038 Raw data (stat): 27034 (minisat+_script) S 27033 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842071962 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.009 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 27038 Raw data (stat): 27034 (minisat+_script) S 27033 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842071962 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.4211 s] Raw data (loadavg): 0.95 0.97 0.91 1/53 27038 Raw data (stat): 27034 (minisat+_script) S 27033 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842071962 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 30 Real time (s): 30.4208 CPU time (s): 30.3834 CPU user time (s): 30.3294 CPU system time (s): 0.053991 CPU usage (%): 99.877 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 344750 #### END VERIFIER DATA ####