Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-markshare1.opb |
MD5SUM | ba87f5dfbaed559dc55bc00bf07dc880 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3712 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 120 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 6291450 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 6291450 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.68 |
Number of variables | 170 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 70 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc25 THE 2005-05-27 09:38:24 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23780 boxname=wulflinc25 idbench=1424 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ba87f5dfbaed559dc55bc00bf07dc880 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-markshare1.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-markshare1.opb IDLAUNCH: 23780 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 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.220 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 899612 kB Buffers: 2000 kB Cached: 113704 kB SwapCached: 984 kB Active: 18868 kB Inactive: 98848 kB HighTotal: 131008 kB HighFree: 14504 kB LowTotal: 903652 kB LowFree: 885108 kB SwapTotal: 2097892 kB SwapFree: 2095960 kB Dirty: 28 kB Writeback: 0 kB Mapped: 4976 kB Slab: 11612 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 09:58:54 (client local time) WITH STATUS 152 IN 1229.86 SECONDS stats: 23780 7 1229.86 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 12 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 10]---> BDD-cost:23437 c ---[ 8]---> BDD-cost:28407 c ---[ 6]---> BDD-cost:25972 c ---[ 4]---> BDD-cost:24798 c ---[ 2]---> BDD-cost:25031 c ---[ 0]---> BDD-cost:24117 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 436749 1274733 | 145583 0 0 nan | 0.000 % | c | 100 | 436749 1274733 | 160141 100 9403 94.0 | 0.012 % | c ============================================================================== c [1mFound solution: 862848[0m c ---[ 0]---> Sorter-cost: 1464 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 | 102 | 440476 1283432 | 146825 102 9461 92.8 | 0.012 % | c ============================================================================== c [1mFound solution: 860928[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 | 105 | 440500 1283513 | 146833 105 9619 91.6 | 0.012 % | c ============================================================================== c [1mFound solution: 848640[0m c ---[ 0]---> Sorter-cost: 7 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 | 106 | 440508 1283534 | 146836 106 9694 91.5 | 0.012 % | c ============================================================================== c [1mFound solution: 839296[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 | 109 | 440517 1283557 | 146839 109 9892 90.8 | 0.012 % | c ============================================================================== c [1mFound solution: 835328[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 | 112 | 440525 1283579 | 146841 112 10046 89.7 | 0.012 % | c ============================================================================== c [1mFound solution: 811776[0m c ---[ 0]---> Sorter-cost: 5 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 | 115 | 440531 1283593 | 146843 115 10228 88.9 | 0.012 % | c ============================================================================== c [1mFound solution: 793344[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 | 138 | 440541 1283616 | 146847 138 11635 84.3 | 0.012 % | c ============================================================================== c [1mFound solution: 788224[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 | 193 | 440551 1283638 | 146850 193 14480 75.0 | 0.012 % | c ============================================================================== c [1mFound solution: 784256[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 | 198 | 440561 1283669 | 146853 198 14774 74.6 | 0.012 % | c ============================================================================== c [1mFound solution: 760704[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 | 199 | 440572 1283698 | 146857 199 14819 74.5 | 0.012 % | c ============================================================================== c [1mFound solution: 760064[0m c ---[ 0]---> Sorter-cost: 10 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 | 222 | 440584 1283728 | 146861 222 15796 71.2 | 0.012 % | c ============================================================================== c [1mFound solution: 755840[0m c ---[ 0]---> Sorter-cost: 10 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 | 271 | 440596 1283756 | 146865 271 18033 66.5 | 0.012 % | c ============================================================================== c [1mFound solution: 740864[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 | 330 | 440609 1283788 | 146869 330 20875 63.3 | 0.012 % | c ============================================================================== c [1mFound solution: 740224[0m c ---[ 0]---> Sorter-cost: 7 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 | 388 | 440620 1283814 | 146873 388 23291 60.0 | 0.012 % | c ============================================================================== c [1mFound solution: 669184[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 | 392 | 440630 1283839 | 146876 392 23497 59.9 | 0.012 % | c | 493 | 440630 1283839 | 161563 493 25965 52.7 | 0.022 % | c | 645 | 440630 1283839 | 177719 645 38402 59.5 | 0.022 % | c | 870 | 440630 1283839 | 195491 870 49510 56.9 | 0.022 % | c | 1208 | 440630 1283839 | 215041 1208 64325 53.2 | 0.022 % | c ============================================================================== c [1mFound solution: 619392[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 | 1350 | 440647 1283882 | 146882 1350 70758 52.4 | 0.022 % | c | 1450 | 440647 1283882 | 161570 1450 75423 52.0 | 0.022 % | c | 1600 | 440647 1283882 | 177727 1600 82144 51.3 | 0.022 % | c | 1826 | 440647 1283882 | 195499 1826 92134 50.5 | 0.022 % | c | 2164 | 440647 1283882 | 215049 2164 108591 50.2 | 0.022 % | c ============================================================================== c [1mFound solution: 616960[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 | 2415 | 440661 1283918 | 146887 2415 120616 49.9 | 0.022 % | c ============================================================================== c [1mFound solution: 612992[0m c ---[ 0]---> Sorter-cost: 7 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 | 2449 | 440671 1283942 | 146890 2449 122229 49.9 | 0.022 % | c ============================================================================== c [1mFound solution: 600448[0m c ---[ 0]---> Sorter-cost: 10 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 | 2513 | 440686 1283977 | 146895 2513 125386 49.9 | 0.022 % | c | 2613 | 440686 1283977 | 161584 2613 129646 49.6 | 0.024 % | c ============================================================================== c [1mFound solution: 594048[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 | 2615 | 440697 1284002 | 146899 2615 129753 49.6 | 0.024 % | c ============================================================================== c [1mFound solution: 593792[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 | 2659 | 440707 1284025 | 146902 2659 131977 49.6 | 0.024 % | c | 2760 | 440707 1284025 | 161592 2760 136347 49.4 | 0.026 % | c | 2911 | 440707 1284025 | 177751 2911 143046 49.1 | 0.026 % | c ============================================================================== c [1mFound solution: 576896[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 | 3074 | 440718 1284052 | 146906 3074 150380 48.9 | 0.026 % | c | 3175 | 440718 1284052 | 161596 3175 153785 48.4 | 0.026 % | c ============================================================================== c [1mFound solution: 576128[0m c ---[ 0]---> Sorter-cost: 6 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 | 3275 | 440725 1284069 | 146908 3275 158596 48.4 | 0.026 % | c | 3377 | 440725 1284069 | 161598 3377 162887 48.2 | 0.027 % | c | 3528 | 440725 1284069 | 177758 3528 168251 47.7 | 0.027 % | c | 3754 | 440725 1284069 | 195534 3754 180561 48.1 | 0.027 % | c ============================================================================== c [1mFound solution: 573568[0m c ---[ 0]---> Sorter-cost: 7 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 | 3791 | 440733 1284088 | 146911 3791 181744 47.9 | 0.027 % | c ============================================================================== c [1mFound solution: 573312[0m c ---[ 0]---> Sorter-cost: 7 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 | 3880 | 440741 1284108 | 146913 3880 185737 47.9 | 0.027 % | c | 3980 | 440741 1284108 | 161604 3980 190136 47.8 | 0.028 % | c ============================================================================== c [1mFound solution: 572288[0m c ---[ 0]---> Sorter-cost: 6 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 | 4008 | 440749 1284127 | 146916 4008 191213 47.7 | 0.028 % | c | 4109 | 440749 1284127 | 161607 4109 195601 47.6 | 0.029 % | c ============================================================================== c [1mFound solution: 566400[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 | 4172 | 440763 1284159 | 146921 4172 198808 47.7 | 0.029 % | c ============================================================================== c [1mFound solution: 566144[0m c ---[ 0]---> Sorter-cost: 7 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 | 4218 | 440773 1284182 | 146924 4218 200938 47.6 | 0.029 % | c ============================================================================== c [1mFound solution: 542848[0m c ---[ 0]---> Sorter-cost: 5 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 | 4228 | 440782 1284202 | 146927 4228 201373 47.6 | 0.029 % | c | 4328 | 440782 1284202 | 161619 4328 205475 47.5 | 0.031 % | c | 4478 | 440782 1284202 | 177781 4478 212196 47.4 | 0.031 % | c ============================================================================== c [1mFound solution: 534400[0m c ---[ 0]---> Sorter-cost: 7 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 | 4640 | 440791 1284222 | 146930 4640 219034 47.2 | 0.031 % | c | 4741 | 440791 1284222 | 161623 4741 223846 47.2 | 0.031 % | c | 4891 | 440791 1284222 | 177785 4891 231251 47.3 | 0.031 % | c | 5116 | 440791 1284222 | 195563 5116 240547 47.0 | 0.031 % | c | 5453 | 440791 1284222 | 215120 5453 255602 46.9 | 0.031 % | c | 5959 | 440791 1284222 | 236632 5959 279577 46.9 | 0.031 % | c | 6720 | 440791 1284222 | 260295 6720 314985 46.9 | 0.031 % | c | 7859 | 440791 1284222 | 286325 7859 369091 47.0 | 0.031 % | c ============================================================================== c [1mFound solution: 531584[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 | 8101 | 440799 1284241 | 146933 8101 380625 47.0 | 0.031 % | c | 8203 | 440799 1284241 | 161626 8203 385228 47.0 | 0.032 % | c ============================================================================== c [1mFound solution: 509312[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 | 8332 | 440811 1284271 | 146937 8332 391378 47.0 | 0.032 % | c | 8432 | 440811 1284271 | 161630 8432 395334 46.9 | 0.033 % | c ============================================================================== c [1mFound solution: 418560[0m c ---[ 0]---> Sorter-cost: 2 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 | 8441 | 440817 1284284 | 146939 8441 395745 46.9 | 0.033 % | c | 8541 | 440817 1284284 | 161632 8541 399910 46.8 | 0.033 % | c ============================================================================== c [1mFound solution: 411264[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 | 8583 | 440828 1284309 | 146942 8583 401708 46.8 | 0.033 % | c | 8683 | 440828 1284309 | 161636 8683 405325 46.7 | 0.034 % | c | 8833 | 440828 1284309 | 177799 8833 412197 46.7 | 0.034 % | c ============================================================================== c [1mFound solution: 408064[0m c ---[ 0]---> Sorter-cost: 7 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 | 8934 | 440835 1284326 | 146945 8934 416333 46.6 | 0.034 % | c ============================================================================== c [1mFound solution: 406016[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 | 8987 | 440844 1284347 | 146948 8987 418999 46.6 | 0.034 % | c ============================================================================== c [1mFound solution: 404608[0m c ---[ 0]---> Sorter-cost: 7 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 | 9069 | 440854 1284370 | 146951 9069 422941 46.6 | 0.034 % | c | 9169 | 440854 1284370 | 161646 9169 427271 46.6 | 0.036 % | c ============================================================================== c [1mFound solution: 401664[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 | 9240 | 440864 1284392 | 146954 9240 430660 46.6 | 0.036 % | c | 9341 | 440864 1284392 | 161649 9341 435483 46.6 | 0.037 % | c ============================================================================== c [1mFound solution: 392064[0m c ---[ 0]---> Sorter-cost: 5 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 | 9444 | 440872 1284413 | 146957 9444 440094 46.6 | 0.037 % | c ============================================================================== c [1mFound solution: 386176[0m c ---[ 0]---> Sorter-cost: 5 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 | 9491 | 440877 1284428 | 146959 9491 442086 46.6 | 0.037 % | c | 9593 | 440877 1284428 | 161654 9593 446226 46.5 | 0.038 % | c | 9743 | 440877 1284428 | 177820 9743 452544 46.4 | 0.038 % | c ============================================================================== c [1mFound solution: 381952[0m c ---[ 0]---> Sorter-cost: 10 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 | 9806 | 440889 1284458 | 146963 9806 455422 46.4 | 0.038 % | c | 9906 | 440889 1284458 | 161659 9906 459239 46.4 | 0.039 % | c ============================================================================== c [1mFound solution: 370176[0m c ---[ 0]---> Sorter-cost: 7 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 | 10008 | 440898 1284480 | 146966 10008 463532 46.3 | 0.039 % | c | 10108 | 440898 1284480 | 161662 10108 467155 46.2 | 0.039 % | c ============================================================================== c [1mFound solution: 369792[0m c ---[ 0]---> Sorter-cost: 3 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 | 10173 | 440902 1284490 | 146967 10173 469622 46.2 | 0.039 % | c | 10273 | 440902 1284490 | 161663 10273 473694 46.1 | 0.040 % | c | 10424 | 440902 1284490 | 177830 10424 479990 46.0 | 0.040 % | c ============================================================================== c [1mFound solution: 366464[0m c ---[ 0]---> Sorter-cost: 6 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 | 10486 | 440910 1284510 | 146970 10486 482731 46.0 | 0.040 % | c | 10586 | 440910 1284510 | 161667 10586 487704 46.1 | 0.041 % | c | 10736 | 440910 1284510 | 177833 10736 495363 46.1 | 0.041 % | c | 10961 | 440910 1284510 | 195617 10961 506231 46.2 | 0.041 % | c | 11300 | 440910 1284510 | 215178 11300 523137 46.3 | 0.041 % | c ============================================================================== c [1mFound solution: 361728[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 | 11531 | 440922 1284538 | 146974 11531 534301 46.3 | 0.041 % | c | 11633 | 440922 1284538 | 161671 11633 538758 46.3 | 0.041 % | c | 11783 | 440922 1284538 | 177838 11783 544623 46.2 | 0.041 % | c ============================================================================== c [1mFound solution: 348800[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 | 11924 | 440934 1284566 | 146978 11924 550662 46.2 | 0.041 % | c | 12024 | 440934 1284566 | 161675 12024 554576 46.1 | 0.042 % | c | 12174 | 440934 1284566 | 177843 12174 561272 46.1 | 0.042 % | c | 12400 | 440934 1284566 | 195627 12400 571437 46.1 | 0.042 % | c ============================================================================== c [1mFound solution: 334976[0m c ---[ 0]---> Sorter-cost: 3 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 | 12500 | 440942 1284584 | 146980 12500 575891 46.1 | 0.042 % | c ============================================================================== c [1mFound solution: 332032[0m c ---[ 0]---> Sorter-cost: 7 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 | 12596 | 440953 1284609 | 146984 12596 579613 46.0 | 0.042 % | c | 12696 | 440953 1284609 | 161682 12696 583453 46.0 | 0.043 % | c | 12847 | 440953 1284609 | 177850 12847 590255 45.9 | 0.043 % | c | 13072 | 440953 1284609 | 195635 13072 599872 45.9 | 0.043 % | c ============================================================================== c [1mFound solution: 329216[0m c ---[ 0]---> Sorter-cost: 6 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 | 13274 | 440961 1284627 | 146987 13274 608552 45.8 | 0.043 % | c | 13374 | 440961 1284627 | 161685 13374 612767 45.8 | 0.044 % | c | 13524 | 440961 1284627 | 177854 13524 619668 45.8 | 0.044 % | c ============================================================================== c [1mFound solution: 319104[0m c ---[ 0]---> Sorter-cost: 7 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 | 13639 | 440969 1284647 | 146989 13639 625710 45.9 | 0.044 % | c | 13739 | 440969 1284647 | 161687 13739 629890 45.8 | 0.044 % | c | 13897 | 440969 1284647 | 177856 13897 637746 45.9 | 0.044 % | c | 14122 | 440969 1284647 | 195642 14122 648374 45.9 | 0.044 % | c ============================================================================== c [1mFound solution: 315904[0m c ---[ 0]---> Sorter-cost: 6 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 | 14372 | 440977 1284667 | 146992 14372 658242 45.8 | 0.044 % | c | 14475 | 440971 1284654 | 161691 14465 662041 45.8 | 0.046 % | c | 14625 | 440971 1284654 | 177860 14615 668757 45.8 | 0.046 % | c ============================================================================== c [1mFound solution: 304768[0m c ---[ 0]---> Sorter-cost: 6 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 | 14711 | 440982 1284679 | 146994 14701 672283 45.7 | 0.046 % | c | 14816 | 440982 1284679 | 161693 14806 677451 45.8 | 0.047 % | c | 14966 | 440982 1284679 | 177862 14956 683533 45.7 | 0.047 % | c | 15191 | 440982 1284679 | 195649 15181 692486 45.6 | 0.047 % | c | 15528 | 440982 1284679 | 215213 15518 709146 45.7 | 0.047 % | c ============================================================================== c [1mFound solution: 299776[0m c ---[ 0]---> Sorter-cost: 6 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 | 15644 | 440991 1284700 | 146997 15634 713370 45.6 | 0.047 % | c | 15744 | 440991 1284700 | 161696 15734 717890 45.6 | 0.048 % | c | 15897 | 440991 1284700 | 177866 15887 725496 45.7 | 0.048 % | c | 16122 | 440991 1284700 | 195653 16112 739108 45.9 | 0.048 % | c ============================================================================== c [1mFound solution: 290944[0m c ---[ 0]---> Sorter-cost: 6 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 | 16208 | 440997 1284715 | 146999 16198 742649 45.8 | 0.048 % | c | 16308 | 440997 1284715 | 161698 16298 746278 45.8 | 0.048 % | c | 16458 | 440997 1284715 | 177868 16448 751421 45.7 | 0.048 % | c | 16683 | 440997 1284715 | 195655 16673 761580 45.7 | 0.048 % | c ============================================================================== c [1mFound solution: 290432[0m c ---[ 0]---> Sorter-cost: 6 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 | 16824 | 441005 1284734 | 147001 16814 767918 45.7 | 0.048 % | c | 16925 | 441005 1284734 | 161701 16915 773134 45.7 | 0.049 % | c | 17076 | 441005 1284734 | 177871 17066 779868 45.7 | 0.049 % | c ============================================================================== c [1mFound solution: 274816[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 | 17259 | 441014 1284755 | 147004 17249 787911 45.7 | 0.049 % | c ============================================================================== c [1mFound solution: 274304[0m c ---[ 0]---> Sorter-cost: 6 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 | 17335 | 441023 1284775 | 147007 17325 791218 45.7 | 0.049 % | c | 17435 | 441023 1284775 | 161707 17425 794011 45.6 | 0.050 % | c | 17585 | 441023 1284775 | 177878 17575 801040 45.6 | 0.050 % | c | 17810 | 441023 1284775 | 195666 17800 811743 45.6 | 0.050 % | c | 18147 | 441015 1284757 | 215232 18136 828050 45.7 | 0.052 % | c ============================================================================== c [1mFound solution: 273152[0m c ---[ 0]---> Sorter-cost: 7 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 | 18499 | 441025 1284780 | 147008 18488 843222 45.6 | 0.052 % | c | 18599 | 441025 1284780 | 161708 18588 846957 45.6 | 0.052 % | c | 18749 | 441025 1284780 | 177879 18738 853828 45.6 | 0.052 % | c ============================================================================== c [1mFound solution: 272256[0m c ---[ 0]---> Sorter-cost: 2 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 | 18857 | 441032 1284795 | 147010 18846 858450 45.6 | 0.052 % | c | 18957 | 441032 1284795 | 161711 18946 863843 45.6 | 0.053 % | c | 19107 | 441032 1284795 | 177882 19096 869575 45.5 | 0.053 % | c ============================================================================== c [1mFound solution: 272128[0m c ---[ 0]---> Sorter-cost: 6 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 | 19272 | 441042 1284817 | 147014 19261 877445 45.6 | 0.053 % | c | 19372 | 441042 1284817 | 161715 19361 882035 45.6 | 0.054 % | c ============================================================================== c [1mFound solution: 262400[0m c ---[ 0]---> Sorter-cost: 6 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 | 19382 | 441049 1284832 | 147016 19371 882452 45.6 | 0.054 % | c | 19484 | 441049 1284832 | 161717 19473 887084 45.6 | 0.054 % | c ============================================================================== c [1mFound solution: 246400[0m c ---[ 0]---> Sorter-cost: 7 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 | 19624 | 441058 1284854 | 147019 19613 893335 45.5 | 0.054 % | c | 19725 | 441058 1284854 | 161720 19714 897482 45.5 | 0.055 % | c | 19875 | 441058 1284854 | 177892 19864 911553 45.9 | 0.055 % | c | 20101 | 441058 1284854 | 195682 20090 919918 45.8 | 0.055 % | c ============================================================================== c [1mFound solution: 241536[0m c ---[ 0]---> Sorter-cost: 4 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 | 20304 | 441064 1284869 | 147021 20293 928231 45.7 | 0.055 % | c | 20404 | 441064 1284869 | 161723 20393 931629 45.7 | 0.056 % | c ============================================================================== c [1mFound solution: 240128[0m c ---[ 0]---> Sorter-cost: 5 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 | 20439 | 441071 1284887 | 147023 20428 932792 45.7 | 0.056 % | c | 20539 | 441071 1284887 | 161725 20528 937206 45.7 | 0.056 % | c ============================================================================== c [1mFound solution: 235264[0m c ---[ 0]---> Sorter-cost: 7 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 | 20688 | 441081 1284911 | 147027 20677 944124 45.7 | 0.056 % | c ============================================================================== c [1mFound solution: 230400[0m c ---[ 0]---> Sorter-cost: 7 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 | 20751 | 441089 1284930 | 147029 20740 946610 45.6 | 0.056 % | c ============================================================================== c [1mFound solution: 211968[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 | 20777 | 441097 1284951 | 147032 20766 947909 45.6 | 0.056 % | c | 20877 | 441097 1284951 | 161735 20866 951420 45.6 | 0.058 % | c ============================================================================== c [1mFound solution: 205568[0m c ---[ 0]---> Sorter-cost: 2 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 | 20996 | 441100 1284958 | 147033 20985 957006 45.6 | 0.058 % | c | 21096 | 441100 1284958 | 161736 21085 960796 45.6 | 0.059 % | c | 21248 | 441100 1284958 | 177909 21237 967199 45.5 | 0.059 % | c | 21475 | 441100 1284958 | 195700 21464 976785 45.5 | 0.059 % | c ============================================================================== c [1mFound solution: 185472[0m c ---[ 0]---> Sorter-cost: 7 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 | 21659 | 441110 1284982 | 147036 21648 983981 45.5 | 0.059 % | c | 21759 | 441097 1284955 | 161739 21715 986335 45.4 | 0.062 % | c | 21909 | 441097 1284955 | 177913 21865 991891 45.4 | 0.062 % | c | 22134 | 441097 1284955 | 195704 22090 1000890 45.3 | 0.062 % | c | 22471 | 441097 1284955 | 215275 22427 1015061 45.3 | 0.062 % | c ============================================================================== c [1mFound solution: 183296[0m c ---[ 0]---> Sorter-cost: 7 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 | 22595 | 441106 1284977 | 147035 22551 1020658 45.3 | 0.062 % | c ============================================================================== c [1mFound solution: 153216[0m c ---[ 0]---> Sorter-cost: 7 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 | 22689 | 441117 1285002 | 147039 22645 1024070 45.2 | 0.062 % | c | 22794 | 441117 1285002 | 161742 22750 1027704 45.2 | 0.063 % | c | 22945 | 441117 1285002 | 177917 22901 1033448 45.1 | 0.063 % | c ============================================================================== c [1mFound solution: 149888[0m c ---[ 0]---> Sorter-cost: 6 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 | 23023 | 441125 1285020 | 147041 22979 1036578 45.1 | 0.063 % | c | 23125 | 441125 1285020 | 161745 23081 1041029 45.1 | 0.064 % | c | 23275 | 441125 1285020 | 177919 23231 1050876 45.2 | 0.064 % | c ============================================================================== c [1mFound solution: 145024[0m c ---[ 0]---> Sorter-cost: 6 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 | 23385 | 441132 1285036 | 147044 23341 1055448 45.2 | 0.064 % | c | 23485 | 441132 1285036 | 161748 23441 1059200 45.2 | 0.065 % | c ============================================================================== c [1mFound solution: 133248[0m c ---[ 0]---> Sorter-cost: 4 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 | 23491 | 441137 1285047 | 147045 23447 1059434 45.2 | 0.065 % | c | 23592 | 441137 1285047 | 161749 23548 1062900 45.1 | 0.065 % | c | 23742 | 441137 1285047 | 177924 23698 1072862 45.3 | 0.065 % | c | 23968 | 441137 1285047 | 195716 23924 1082499 45.2 | 0.065 % | c | 24305 | 441133 1285038 | 215288 24259 1098101 45.3 | 0.066 % | c ============================================================================== c [1mFound solution: 130688[0m c ---[ 0]---> Sorter-cost: 5 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 | 24656 | 441100 1284953 | 147033 23871 1089236 45.6 | 0.066 % | c | 24756 | 441100 1284953 | 161736 23971 1093219 45.6 | 0.076 % | c ============================================================================== c [1mFound solution: 129280[0m c ---[ 0]---> Sorter-cost: 5 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 | 24893 | 441104 1284965 | 147034 24108 1099317 45.6 | 0.076 % | c | 24993 | 441104 1284965 | 161737 24208 1103007 45.6 | 0.077 % | c | 25143 | 441095 1284946 | 177911 24020 1095893 45.6 | 0.078 % | c ============================================================================== c [1mFound solution: 121728[0m c ---[ 0]---> Sorter-cost: 4 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 | 25230 | 441100 1284959 | 147033 24107 1099504 45.6 | 0.078 % | c ============================================================================== c [1mFound solution: 121344[0m c ---[ 0]---> Sorter-cost: 5 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 | 25288 | 441106 1284975 | 147035 24165 1101566 45.6 | 0.078 % | c | 25388 | 441106 1284975 | 161738 24265 1105059 45.5 | 0.080 % | c ============================================================================== c [1mFound solution: 120960[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 | 25496 | 441112 1284991 | 147037 24373 1109073 45.5 | 0.080 % | c | 25597 | 441112 1284991 | 161740 24474 1112801 45.5 | 0.080 % | c ============================================================================== c [1mFound solution: 86016[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 | 25667 | 441122 1285014 | 147040 24544 1114984 45.4 | 0.080 % | c | 25768 | 441122 1285014 | 161744 24645 1118887 45.4 | 0.081 % | c | 25919 | 441122 1285014 | 177918 24796 1124465 45.3 | 0.081 % | c ============================================================================== c [1mFound solution: 85760[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 | 25980 | 441130 1285033 | 147043 24857 1126707 45.3 | 0.081 % | c ============================================================================== c [1mFound solution: 83968[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 | 25984 | 441140 1285056 | 147046 24861 1126770 45.3 | 0.081 % | c ============================================================================== c [1mFound solution: 81536[0m c ---[ 0]---> Sorter-cost: 4 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 | 26005 | 441145 1285068 | 147048 24882 1127820 45.3 | 0.081 % | c ============================================================================== c [1mFound solution: 77568[0m c ---[ 0]---> Sorter-cost: 5 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 | 26038 | 441152 1285084 | 147050 24915 1128883 45.3 | 0.081 % | c | 26138 | 441152 1285084 | 161755 25015 1132458 45.3 | 0.084 % | c ============================================================================== c [1mFound solution: 75264[0m c ---[ 0]---> Sorter-cost: 3 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 | 26253 | 441155 1285091 | 147051 25130 1136516 45.2 | 0.084 % | c | 26354 | 441155 1285091 | 161756 25231 1140043 45.2 | 0.084 % | c | 26504 | 441155 1285091 | 177931 25381 1146202 45.2 | 0.084 % | c | 26729 | 441155 1285091 | 195724 25606 1154457 45.1 | 0.084 % | c ============================================================================== c [1mFound solution: 66816[0m c ---[ 0]---> Sorter-cost: 3 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 | 26850 | 441158 1285098 | 147052 25727 1158926 45.0 | 0.084 % | c | 26951 | 441158 1285098 | 161757 25828 1162787 45.0 | 0.085 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 29359 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.95 0.90 2/54 29355 Raw data (stat): 29355 (runsolver) R 29354 1586 1585 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855157183 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10 s] Raw data (loadavg): 0.93 0.95 0.90 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+19.9999 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0005 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+39.9998 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+49.9997 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+59.9999 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+69.9996 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0004 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+89.9998 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+99.9994 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+149.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+159.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+169.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+179.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+209.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+219.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+229.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+239.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+249.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+259.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+269.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+279.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+289.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+299.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+309.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+319.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+329.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+339.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+349.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+359.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+369.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+379.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+389.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+399.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+409.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+419.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+429.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+439.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+449.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+459.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+469.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+479.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+489.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+499.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+509.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+519.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+529.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+539.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+549.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+559.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+569.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+579.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+589.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+599.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+609.993 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+619.993 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+629.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+639.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+649.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+659.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+669.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+679.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+689.993 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+699.993 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+709.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+719.993 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+729.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+739.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+749.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+759.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+769.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+779.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+789.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+799.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+809.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+819.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+829.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+839.991 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+849.991 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+859.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+869.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+879.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+889.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+899.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+909.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+919.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+929.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+939.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+949.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+959.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+969.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+979.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+989.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+999.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1009.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1019.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1029.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1039.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1049.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1059.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1069.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1079.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1089.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1099.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1109.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1119.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1129.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1139.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1149.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1159.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1169.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1179.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1189.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.67 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 29359 Raw data (stat): 29355 (minisat+_script) S 29354 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855157183 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.67 CPU time (s): 1229.86 CPU user time (s): 1229.45 CPU system time (s): 0.414936 CPU usage (%): 100.015 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####