Name | mps-v2-13-7/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-13-7-maros.opb |
MD5SUM | 1ae5b04b2d0e1f5ab82e29e98b8350c0 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 43097 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 64 |
Biggest coefficient in the objective function | 4718592 |
Number of bits for the biggest coefficient in the objective function | 23 |
Sum of the numbers in the objective function | 14745570 |
Number of bits of the sum of numbers in the objective function | 24 |
Biggest number in a constraint | 4718592 |
Number of bits of the biggest number in a constraint | 23 |
Biggest sum of numbers in a constraint | 14745570 |
Number of bits of the biggest sum of numbers | 24 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 23.3694 |
Number of variables | 64 |
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 | 12 |
Maximum length of a constraint | 64 |
LAUNCH ON wulflinc8 THE 2005-09-20 05:53:31 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3515 boxname=wulflinc8 idbench=1171 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1ae5b04b2d0e1f5ab82e29e98b8350c0 /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-maros.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-maros.opb IDLAUNCH: 3515 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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: 868140 kB Buffers: 24944 kB Cached: 115348 kB SwapCached: 876 kB Active: 40268 kB Inactive: 102788 kB HighTotal: 131008 kB HighFree: 20552 kB LowTotal: 903652 kB LowFree: 847588 kB SwapTotal: 2097136 kB SwapFree: 2095848 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5764 kB Slab: 17904 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 05:53:55 (client local time) WITH STATUS 30 IN 23.3694 SECONDS stats: 3515 0 23.3694 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: 11 c ---[ 3]---> Sorter-cost: 961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 410 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 1]---> Sorter-cost: 429 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 4455 10455 | 1485 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 54221[0m c ---[ 0]---> Sorter-cost: 988 Base: 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 | 94 | 6727 15762 | 2242 94 1453 15.5 | 0.000 % | c ============================================================================== c [1mFound solution: 53679[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 111 | 6745 15831 | 2248 111 1578 14.2 | 0.000 % | c ============================================================================== c [1mFound solution: 49212[0m c ---[ 0]---> Sorter-cost: 14 Base: 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 | 139 | 6773 15898 | 2257 139 1822 13.1 | 0.000 % | c | 239 | 6773 15898 | 2482 239 3347 14.0 | 1.048 % | c | 390 | 6773 15898 | 2730 390 5135 13.2 | 1.049 % | c | 618 | 6773 15898 | 3004 618 8483 13.7 | 1.048 % | c | 955 | 6773 15898 | 3304 955 15439 16.2 | 1.049 % | c | 1461 | 6773 15898 | 3634 1461 23005 15.7 | 1.049 % | c ============================================================================== c [1mFound solution: 49121[0m c ---[ 0]---> Sorter-cost: 13 Base: 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 | 1506 | 6779 15924 | 2259 1506 23500 15.6 | 1.049 % | c | 1606 | 6779 15924 | 2484 1606 24721 15.4 | 1.087 % | c ============================================================================== c [1mFound solution: 47761[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 1618 | 6796 15965 | 2265 1618 24822 15.3 | 1.087 % | c | 1718 | 6796 15965 | 2491 1718 27411 16.0 | 1.122 % | c | 1869 | 6796 15965 | 2740 1869 30380 16.3 | 1.123 % | c | 2095 | 6796 15965 | 3014 2095 35545 17.0 | 1.122 % | c ============================================================================== c [1mFound solution: 47583[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 2375 | 6805 15990 | 2268 2375 41355 17.4 | 1.122 % | c | 2476 | 6802 15984 | 2494 1287 20378 15.8 | 1.201 % | c | 2627 | 6802 15984 | 2744 1438 22436 15.6 | 1.200 % | c ============================================================================== c [1mFound solution: 47072[0m c ---[ 0]---> Sorter-cost: 13 Base: 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 | 2802 | 6811 16012 | 2270 1613 24999 15.5 | 1.200 % | c | 2902 | 6811 16012 | 2497 1713 27087 15.8 | 1.240 % | c | 3052 | 6811 16012 | 2746 1863 29554 15.9 | 1.238 % | c ============================================================================== c [1mFound solution: 46956[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 3077 | 6822 16040 | 2274 1888 30004 15.9 | 1.238 % | c ============================================================================== c [1mFound solution: 46814[0m c ---[ 0]---> Sorter-cost: 14 Base: 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 | 3107 | 6836 16077 | 2278 1918 30451 15.9 | 1.238 % | c ============================================================================== c [1mFound solution: 46810[0m c ---[ 0]---> Sorter-cost: 13 Base: 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 | 3132 | 6848 16109 | 2282 1943 30841 15.9 | 1.238 % | c | 3232 | 6848 16109 | 2510 2043 32526 15.9 | 1.347 % | c | 3382 | 6848 16109 | 2761 2193 34455 15.7 | 1.347 % | c | 3608 | 6848 16109 | 3037 2419 37161 15.4 | 1.347 % | c ============================================================================== c [1mFound solution: 46758[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 3671 | 6861 16140 | 2287 2482 38274 15.4 | 1.347 % | c | 3772 | 6861 16140 | 2515 1342 14247 10.6 | 1.384 % | c ============================================================================== c [1mFound solution: 45478[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 3782 | 6869 16158 | 2289 1352 14384 10.6 | 1.384 % | c | 3884 | 6869 16158 | 2517 1454 16340 11.2 | 1.421 % | c | 4039 | 6869 16158 | 2769 1609 18375 11.4 | 1.421 % | c | 4265 | 6869 16158 | 3046 1835 21428 11.7 | 1.421 % | c ============================================================================== c [1mFound solution: 45262[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 4347 | 6881 16187 | 2293 1917 23553 12.3 | 1.421 % | c | 4452 | 6881 16187 | 2522 2022 24947 12.3 | 1.458 % | c | 4602 | 6881 16187 | 2774 2172 27451 12.6 | 1.458 % | c | 4828 | 6881 16187 | 3051 2398 30681 12.8 | 1.458 % | c | 5167 | 6881 16187 | 3357 2737 36497 13.3 | 1.458 % | c | 5675 | 6881 16187 | 3692 3245 45663 14.1 | 1.458 % | c | 6434 | 6881 16187 | 4062 2014 26572 13.2 | 1.458 % | c | 7575 | 6881 16187 | 4468 3155 45341 14.4 | 1.458 % | c ============================================================================== c [1mFound solution: 45261[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 8894 | 6890 16209 | 2296 4474 73429 16.4 | 1.458 % | c ============================================================================== c [1mFound solution: 44828[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 8914 | 6901 16240 | 2300 2257 32085 14.2 | 1.458 % | c | 9015 | 6901 16240 | 2530 2358 33311 14.1 | 1.531 % | c | 9165 | 6901 16240 | 2783 2508 36275 14.5 | 1.531 % | c | 9391 | 6901 16240 | 3061 2734 39188 14.3 | 1.531 % | c | 9730 | 6901 16240 | 3367 3073 44267 14.4 | 1.531 % | c | 10237 | 6901 16240 | 3704 3580 54280 15.2 | 1.531 % | c | 11000 | 6901 16240 | 4074 2394 29965 12.5 | 1.531 % | c | 12141 | 6901 16240 | 4482 3535 51793 14.7 | 1.531 % | c ============================================================================== c [1mFound solution: 44769[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 13520 | 6908 16263 | 2302 2556 27442 10.7 | 1.531 % | c | 13621 | 6908 16263 | 2532 1379 10990 8.0 | 1.567 % | c | 13771 | 6908 16263 | 2785 1529 13596 8.9 | 1.567 % | c | 13996 | 6908 16263 | 3063 1754 17123 9.8 | 1.567 % | c ============================================================================== c [1mFound solution: 44721[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 14120 | 6917 16288 | 2305 1878 18313 9.8 | 1.567 % | c ============================================================================== c [1mFound solution: 44449[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 14132 | 6927 16316 | 2309 1890 18602 9.8 | 1.567 % | c | 14234 | 6927 16316 | 2539 1992 20732 10.4 | 1.637 % | c ============================================================================== c [1mFound solution: 44293[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 14349 | 6941 16350 | 2313 2107 23370 11.1 | 1.637 % | c | 14449 | 6941 16350 | 2544 2207 25213 11.4 | 1.671 % | c | 14600 | 6941 16350 | 2798 2358 27396 11.6 | 1.671 % | c | 14825 | 6941 16350 | 3078 2583 30696 11.9 | 1.671 % | c | 15162 | 6941 16350 | 3386 2920 36694 12.6 | 1.671 % | c | 15668 | 6941 16350 | 3725 3426 45563 13.3 | 1.671 % | c ============================================================================== c [1mFound solution: 44052[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 15868 | 6953 16380 | 2317 3626 50124 13.8 | 1.671 % | c | 15969 | 6953 16380 | 2548 1914 20129 10.5 | 1.706 % | c | 16121 | 6953 16380 | 2803 2066 21969 10.6 | 1.706 % | c | 16347 | 6953 16380 | 3083 2292 26233 11.4 | 1.706 % | c ============================================================================== c [1mFound solution: 44048[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 16545 | 6966 16413 | 2322 2490 29607 11.9 | 1.706 % | c | 16648 | 6966 16413 | 2554 1348 11205 8.3 | 1.740 % | c | 16798 | 6966 16413 | 2809 1498 13726 9.2 | 1.740 % | c | 17025 | 6966 16413 | 3090 1725 17757 10.3 | 1.740 % | c | 17365 | 6947 16371 | 3399 2064 22105 10.7 | 1.933 % | c | 17874 | 6947 16371 | 3739 2573 31541 12.3 | 1.933 % | c | 18634 | 6947 16371 | 4113 3333 43616 13.1 | 1.933 % | c ============================================================================== c [1mFound solution: 44046[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 19334 | 6957 16396 | 2319 4033 55712 13.8 | 1.933 % | c | 19438 | 6957 16396 | 2550 2121 23415 11.0 | 1.968 % | c | 19591 | 6957 16396 | 2805 2274 25207 11.1 | 1.968 % | c ============================================================================== c [1mFound solution: 44044[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 19787 | 6969 16425 | 2323 2470 27993 11.3 | 1.968 % | c | 19887 | 6969 16425 | 2555 1335 10218 7.7 | 2.002 % | c ============================================================================== c [1mFound solution: 44034[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 19982 | 6980 16453 | 2326 1430 12648 8.8 | 2.002 % | c | 20082 | 6980 16453 | 2558 1530 13615 8.9 | 2.037 % | c | 20232 | 6891 16251 | 2814 1506 13776 9.1 | 3.035 % | c | 20458 | 6891 16251 | 3095 1732 15889 9.2 | 3.037 % | c ============================================================================== c [1mFound solution: 44025[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 20513 | 6843 16144 | 2281 1453 12699 8.7 | 3.037 % | c | 20614 | 6843 16144 | 2509 1554 14048 9.0 | 3.755 % | c ============================================================================== c [1mFound solution: 44006[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 20693 | 6852 16166 | 2284 1633 15691 9.6 | 3.755 % | c | 20793 | 6852 16166 | 2512 1733 17138 9.9 | 3.788 % | c | 20943 | 6852 16166 | 2763 1883 19668 10.4 | 3.788 % | c | 21168 | 6852 16166 | 3040 2108 23643 11.2 | 3.788 % | c | 21506 | 6852 16166 | 3344 2446 29003 11.9 | 3.788 % | c ============================================================================== c [1mFound solution: 44004[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 21585 | 6863 16192 | 2287 2525 30129 11.9 | 3.788 % | c ============================================================================== c [1mFound solution: 44003[0m c ---[ 0]---> Sorter-cost: 4 Base: 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 | 21600 | 6867 16203 | 2289 1278 9814 7.7 | 3.788 % | c ============================================================================== c [1mFound solution: 43993[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 21604 | 6874 16225 | 2291 1282 9859 7.7 | 3.788 % | c ============================================================================== c [1mFound solution: 43934[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 21608 | 6884 16253 | 2294 1286 9892 7.7 | 3.788 % | c ============================================================================== c [1mFound solution: 43669[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 21617 | 6899 16290 | 2299 1295 10077 7.8 | 3.788 % | c ============================================================================== c [1mFound solution: 43661[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 21633 | 6912 16322 | 2304 1311 10473 8.0 | 3.788 % | c ============================================================================== c [1mFound solution: 43486[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 21710 | 6920 16342 | 2306 1388 11165 8.0 | 3.788 % | c | 21810 | 6920 16342 | 2536 1488 13394 9.0 | 3.990 % | c | 21960 | 6920 16342 | 2790 1638 15643 9.6 | 3.990 % | c | 22187 | 6920 16342 | 3069 1865 19235 10.3 | 3.990 % | c | 22524 | 6920 16342 | 3376 2202 24208 11.0 | 3.990 % | c ============================================================================== c [1mFound solution: 43484[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 22933 | 6928 16364 | 2309 2611 29688 11.4 | 3.990 % | c | 23034 | 6928 16364 | 2539 1407 11887 8.4 | 4.020 % | c | 23184 | 6928 16364 | 2793 1557 14910 9.6 | 4.020 % | c ============================================================================== c [1mFound solution: 43482[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 23277 | 6936 16384 | 2312 1650 16240 9.8 | 4.020 % | c | 23378 | 6936 16384 | 2543 1751 17937 10.2 | 4.050 % | c | 23530 | 6936 16384 | 2797 1903 20380 10.7 | 4.050 % | c | 23756 | 6936 16384 | 3077 2129 24543 11.5 | 4.050 % | c | 24094 | 6936 16384 | 3384 2467 30002 12.2 | 4.050 % | c ============================================================================== c [1mFound solution: 43459[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 24222 | 6944 16406 | 2314 2595 32414 12.5 | 4.050 % | c | 24322 | 6944 16406 | 2545 1398 12737 9.1 | 4.079 % | c | 24474 | 6944 16406 | 2799 1550 15698 10.1 | 4.079 % | c | 24700 | 6944 16406 | 3079 1776 21704 12.2 | 4.079 % | c | 25037 | 6944 16406 | 3387 2113 27209 12.9 | 4.080 % | c | 25544 | 6944 16406 | 3726 2620 36137 13.8 | 4.080 % | c | 26303 | 6944 16406 | 4099 3379 52722 15.6 | 4.080 % | c ============================================================================== c [1mFound solution: 43458[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 26492 | 6954 16432 | 2318 3568 57336 16.1 | 4.080 % | c | 26593 | 6954 16432 | 2549 1885 23996 12.7 | 4.108 % | c | 26744 | 6954 16432 | 2804 2036 26513 13.0 | 4.108 % | c ============================================================================== c [1mFound solution: 43457[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 26790 | 6965 16461 | 2321 2082 27489 13.2 | 4.108 % | c ============================================================================== c [1mFound solution: 43450[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 26801 | 6976 16490 | 2325 2093 27619 13.2 | 4.108 % | c ============================================================================== c [1mFound solution: 43448[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 26802 | 6990 16526 | 2330 2094 27687 13.2 | 4.108 % | c ============================================================================== c [1mFound solution: 43443[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 26874 | 7000 16552 | 2333 2166 28924 13.4 | 4.108 % | c | 26974 | 7000 16552 | 2566 2266 31765 14.0 | 4.211 % | c | 27124 | 7000 16552 | 2822 2416 34979 14.5 | 4.211 % | c | 27351 | 7000 16552 | 3105 2643 39418 14.9 | 4.211 % | c | 27689 | 7000 16552 | 3415 2981 46999 15.8 | 4.212 % | c | 28197 | 7000 16552 | 3757 3489 55560 15.9 | 4.211 % | c ============================================================================== c [1mFound solution: 43209[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 28793 | 7011 16580 | 2337 4085 66559 16.3 | 4.211 % | c | 28895 | 7011 16580 | 2570 2145 25876 12.1 | 4.239 % | c | 29045 | 7011 16580 | 2827 2295 28083 12.2 | 4.239 % | c | 29270 | 7011 16580 | 3110 2520 31760 12.6 | 4.239 % | c | 29610 | 7011 16580 | 3421 2860 37337 13.1 | 4.239 % | c ============================================================================== c [1mFound solution: 43206[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 29717 | 7023 16610 | 2341 2967 38797 13.1 | 4.239 % | c | 29818 | 7023 16610 | 2575 1585 14362 9.1 | 4.267 % | c | 29968 | 7023 16610 | 2832 1735 16833 9.7 | 4.266 % | c ============================================================================== c [1mFound solution: 43205[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 30043 | 7032 16633 | 2344 1810 18082 10.0 | 4.266 % | c | 30143 | 7032 16633 | 2578 1910 19927 10.4 | 4.295 % | c | 30294 | 7032 16633 | 2836 2061 23204 11.3 | 4.295 % | c | 30523 | 7032 16633 | 3119 2290 26886 11.7 | 4.295 % | c ============================================================================== c [1mFound solution: 43198[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 30764 | 7044 16663 | 2348 2531 32302 12.8 | 4.295 % | c | 30866 | 7044 16663 | 2582 1368 12482 9.1 | 4.321 % | c | 31017 | 6806 16139 | 2841 1415 13491 9.5 | 6.591 % | c | 31242 | 6806 16139 | 3125 1640 16844 10.3 | 6.591 % | c ============================================================================== c [1mFound solution: 43195[0m c ---[ 0]---> Sorter-cost: 270 Base: 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 | 31554 | 7426 17584 | 2475 1952 23389 12.0 | 6.591 % | c | 31654 | 7426 17584 | 2722 2052 26063 12.7 | 6.127 % | c | 31804 | 7426 17584 | 2994 2202 28729 13.0 | 6.127 % | c ============================================================================== c [1mFound solution: 43193[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 31912 | 7440 17619 | 2480 2310 30666 13.3 | 6.127 % | c | 32012 | 7440 17619 | 2728 2410 33465 13.9 | 6.147 % | c | 32167 | 7440 17619 | 3000 2565 36033 14.0 | 6.147 % | c | 32394 | 7440 17619 | 3300 2792 41647 14.9 | 6.147 % | c | 32731 | 7440 17619 | 3630 3129 46532 14.9 | 6.147 % | c ============================================================================== c [1mFound solution: 43192[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 33234 | 7451 17645 | 2483 3632 56206 15.5 | 6.147 % | c | 33336 | 7451 17645 | 2731 1918 20584 10.7 | 6.170 % | c | 33486 | 7451 17645 | 3004 2068 23457 11.3 | 6.170 % | c | 33712 | 7451 17645 | 3304 2294 28676 12.5 | 6.170 % | c | 34052 | 7451 17645 | 3635 2634 34288 13.0 | 6.170 % | c ============================================================================== c [1mFound solution: 43185[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 34413 | 7460 17665 | 2486 2995 40845 13.6 | 6.170 % | c ============================================================================== c [1mFound solution: 43166[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 34486 | 7471 17690 | 2490 1571 15304 9.7 | 6.170 % | c ============================================================================== c [1mFound solution: 43164[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 34571 | 7484 17719 | 2494 1656 16627 10.0 | 6.170 % | c | 34674 | 7484 17719 | 2743 1759 18442 10.5 | 6.240 % | c | 34824 | 7484 17719 | 3017 1909 20550 10.8 | 6.240 % | c ============================================================================== c [1mFound solution: 43163[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 34996 | 7498 17751 | 2499 2081 23759 11.4 | 6.240 % | c | 35096 | 7498 17751 | 2748 2181 25672 11.8 | 6.259 % | c | 35250 | 7498 17751 | 3023 2335 28041 12.0 | 6.258 % | c | 35475 | 7498 17751 | 3326 2560 32431 12.7 | 6.259 % | c | 35812 | 7498 17751 | 3658 2897 37778 13.0 | 6.259 % | c ============================================================================== c [1mFound solution: 43157[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 36054 | 7507 17771 | 2502 3139 41189 13.1 | 6.259 % | c | 36154 | 7422 17583 | 2752 1350 10584 7.8 | 7.052 % | c | 36307 | 7422 17583 | 3027 1503 12765 8.5 | 7.053 % | c ============================================================================== c [1mFound solution: 43152[0m c ---[ 0]---> Sorter-cost: 461 Base: 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 | 36467 | 8553 20218 | 2851 1663 16026 9.6 | 7.053 % | c | 36567 | 8553 20218 | 3136 1763 18222 10.3 | 6.257 % | c | 36717 | 8553 20218 | 3449 1913 21711 11.3 | 6.258 % | c | 36944 | 8553 20218 | 3794 2140 26141 12.2 | 6.258 % | c ============================================================================== c [1mFound solution: 43151[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 37007 | 8571 20265 | 2857 2203 27326 12.4 | 6.258 % | c | 37107 | 8571 20265 | 3142 2303 28750 12.5 | 6.269 % | c ============================================================================== c [1mFound solution: 43150[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 37179 | 8584 20294 | 2861 2375 30447 12.8 | 6.269 % | c | 37282 | 8584 20294 | 3147 2478 33829 13.7 | 6.287 % | c ============================================================================== c [1mFound solution: 43149[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 37360 | 8595 20319 | 2865 2556 34895 13.7 | 6.287 % | c | 37461 | 8595 20319 | 3151 2657 37342 14.1 | 6.307 % | c | 37611 | 8595 20319 | 3466 2807 40703 14.5 | 6.308 % | c ============================================================================== c [1mFound solution: 43133[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 37820 | 8610 20353 | 2870 3016 45156 15.0 | 6.308 % | c | 37920 | 8610 20353 | 3157 3116 47536 15.3 | 6.323 % | c ============================================================================== c [1mFound solution: 43130[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 38028 | 8623 20382 | 2874 3224 49014 15.2 | 6.323 % | c | 38128 | 8623 20382 | 3161 1712 18271 10.7 | 6.341 % | c | 38279 | 8623 20382 | 3477 1863 20949 11.2 | 6.342 % | c | 38506 | 8623 20382 | 3825 2090 24586 11.8 | 6.341 % | c ============================================================================== c [1mFound solution: 43129[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 38653 | 8636 20411 | 2878 2237 27363 12.2 | 6.341 % | c ============================================================================== c [1mFound solution: 43128[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 38656 | 8649 20440 | 2883 2240 27404 12.2 | 6.341 % | c ============================================================================== c [1mFound solution: 43127[0m c ---[ 0]---> Sorter-cost: 13 Base: 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 | 38742 | 8666 20478 | 2888 2326 28603 12.3 | 6.341 % | c ============================================================================== c [1mFound solution: 43106[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 38786 | 8678 20506 | 2892 2370 29448 12.4 | 6.341 % | c | 38886 | 8678 20506 | 3181 2470 31315 12.7 | 6.412 % | c | 39038 | 8678 20506 | 3499 2622 34693 13.2 | 6.412 % | c | 39263 | 8678 20506 | 3849 2847 38634 13.6 | 6.412 % | c | 39602 | 8678 20506 | 4234 3186 44693 14.0 | 6.412 % | c ============================================================================== c [1mFound solution: 43104[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 39707 | 8690 20535 | 2896 3291 45984 14.0 | 6.412 % | c | 39807 | 8690 20535 | 3185 1746 16737 9.6 | 6.431 % | c ============================================================================== c [1mFound solution: 43103[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 39893 | 8702 20564 | 2900 1832 17762 9.7 | 6.431 % | c ============================================================================== c [1mFound solution: 43101[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 39912 | 8714 20592 | 2904 1851 18000 9.7 | 6.431 % | c ============================================================================== c [1mFound solution: 43100[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 39971 | 8726 20619 | 2908 1910 19127 10.0 | 6.431 % | c | 40071 | 8726 20619 | 3198 2010 21004 10.4 | 6.490 % | c ============================================================================== c [1mFound solution: 43097[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 40081 | 8738 20647 | 2912 2020 21247 10.5 | 6.490 % | c | 40181 | 8738 20647 | 3203 2120 22592 10.7 | 6.509 % | c | 40332 | 8738 20647 | 3523 2271 26073 11.5 | 6.509 % | c | 40558 | 8738 20647 | 3875 2497 29653 11.9 | 6.509 % | c ============================================================================== c [1mOptimal solution: 43097[0m s OPTIMUM FOUND v -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 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 -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_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 : 205 c conflicts : 40757 (1749 /sec) c decisions : 67646 (2903 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 23.3005 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/27859/stat): 27859 (minisat+_script) R 27858 27859 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784375807 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/27859/statm): 174 3 169 147 0 27 0 [pid=27859] 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=27860 New process pid=27861 New process pid=27862 One traced child (pid=27861) exited with status: 0 execve syscall for /bin/sed executable 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=27862) exited with status: 0 One traced child (pid=27860) exited with status: 0 New process pid=27863 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-maros.opb [startup+10.0033 s] Raw data (loadavg): 0.95 0.97 0.91 2/57 27863 Raw data (/proc/27859/stat): 27859 (minisat+_script) S 27858 27859 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1784375807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27859/statm): 531 226 485 147 0 384 0 [pid=27859] vsize: 2124 Raw data (/proc/27863/stat): 27863 (minisat+_64-bit) R 27859 27859 27660 0 -1 0 481 0 0 0 989 2 0 0 25 0 1 0 1784375812 2297856 468 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27863/statm): 561 468 145 145 0 416 0 [pid=27863] vsize: 2244 Current children cumulated CPU time (s) 9.92 Current children cumulated vsize (Kb) 4368 [startup+20.0051 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 27863 Raw data (/proc/27859/stat): 27859 (minisat+_script) S 27858 27859 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1784375807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27859/statm): 531 226 485 147 0 384 0 [pid=27859] vsize: 2124 Raw data (/proc/27863/stat): 27863 (minisat+_64-bit) R 27859 27859 27660 0 -1 0 523 0 0 0 1988 3 0 0 25 0 1 0 1784375812 2457600 510 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27863/statm): 600 510 145 145 0 455 0 [pid=27863] vsize: 2400 Current children cumulated CPU time (s) 19.92 Current children cumulated vsize (Kb) 4524 One traced child (pid=27863) exited with status: 30 One traced child (pid=27859) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 23.4482 CPU time (s): 23.3694 CPU user time (s): 23.3065 CPU system time (s): 0.06299 CPU usage (%): 99.664 Max. virtual memory (cumulated for all children) (Kb): 4524
Verifier: OK 43097