Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-flugpl.opb |
MD5SUM | 1b5898327a7b85a882e36ea549878fdf |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1843200 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 195 |
Biggest coefficient in the objective function | 47185920 |
Number of bits for the biggest coefficient in the objective function | 26 |
Sum of the numbers in the objective function | 103639200 |
Number of bits of the sum of numbers in the objective function | 27 |
Biggest number in a constraint | 78643200 |
Number of bits of the biggest number in a constraint | 27 |
Biggest sum of numbers in a constraint | 159755625 |
Number of bits of the biggest sum of numbers | 28 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.181972 |
Number of variables | 195 |
Total number of constraints | 29 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 29 |
Minimum length of a constraint | 5 |
Maximum length of a constraint | 45 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc30 THE 2005-05-27 09:35:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23769 boxname=wulflinc30 idbench=1413 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1b5898327a7b85a882e36ea549878fdf /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-flugpl.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-flugpl.opb IDLAUNCH: 23769 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 907996 kB Buffers: 2020 kB Cached: 105108 kB SwapCached: 720 kB Active: 17024 kB Inactive: 92168 kB HighTotal: 131008 kB HighFree: 22484 kB LowTotal: 903652 kB LowFree: 885512 kB SwapTotal: 2097892 kB SwapFree: 2096304 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5036 kB Slab: 11796 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 09:35:39 (client local time) WITH STATUS 30 IN 22.0966 SECONDS stats: 23769 0 22.0966 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 35 PB-constraints to clauses... c -- Unit propagations: pp c -- Detecting intervals from adjacent constraints: ##### c -- Clauses(.)/Splits(s): (none) c ---[ 34]---> BDD-cost: 4 c ---[ 33]---> BDD-cost: 4 c ---[ 32]---> BDD-cost: 4 c ---[ 31]---> BDD-cost: 4 c ---[ 30]---> BDD-cost: 4 c ---[ 29]---> BDD-cost: 4 c ---[ 28]---> BDD-cost: 4 c ---[ 27]---> BDD-cost: 4 c ---[ 26]---> BDD-cost: 4 c ---[ 25]---> BDD-cost: 4 c ---[ 24]---> BDD-cost: 4 c ---[ 20]---> BDD-cost: 20 c ---[ 18]---> BDD-cost: 63 c ---[ 16]---> BDD-cost: 63 c ---[ 14]---> BDD-cost: 63 c ---[ 12]---> BDD-cost: 63 c ---[ 11]---> BDD-cost: 107 c ---[ 10]---> BDD-cost: 465 c ---[ 9]---> BDD-cost: 433 c ---[ 8]---> BDD-cost: 476 c ---[ 7]---> BDD-cost: 465 c ---[ 6]---> BDD-cost: 461 c ---[ 5]---> BDD-cost: 17 c ---[ 4]---> BDD-cost: 86 c ---[ 3]---> BDD-cost: 86 c ---[ 2]---> BDD-cost: 86 c ---[ 1]---> BDD-cost: 86 c ---[ 0]---> BDD-cost: 86 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 5452 14681 | 1817 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 2190336[0m c ---[ 0]---> Sorter-cost: 9040 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 | 3 | 28417 68282 | 9472 3 8 2.7 | 0.000 % | c ============================================================================== c [1mFound solution: 2093755[0m c ---[ 0]---> Sorter-cost: 11 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 | 37 | 28458 68526 | 9486 37 1088 29.4 | 0.000 % | c ============================================================================== c [1mFound solution: 2069865[0m c ---[ 0]---> Sorter-cost: 6538 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115 | 41639 99383 | 13879 98 1528 15.6 | 0.000 % | c ============================================================================== c [1mFound solution: 2026841[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 129 | 41682 99554 | 13894 112 1726 15.4 | 0.000 % | c ============================================================================== c [1mFound solution: 2026825[0m c ---[ 0]---> Sorter-cost: 4755 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 | 222 | 48745 116140 | 16248 183 2494 13.6 | 0.000 % | c | 325 | 48745 116140 | 17872 286 6849 23.9 | 10.581 % | c ============================================================================== c [1mFound solution: 2026809[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 453 | 48775 116286 | 16258 414 9877 23.9 | 10.581 % | c ============================================================================== c [1mFound solution: 2025785[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 | 476 | 48785 116310 | 16261 437 10520 24.1 | 10.581 % | c ============================================================================== c [1mFound solution: 2025769[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 499 | 48241 115066 | 16080 450 10620 23.6 | 10.581 % | c ============================================================================== c [1mFound solution: 2023673[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 534 | 48211 115003 | 16070 484 11590 23.9 | 10.581 % | c ============================================================================== c [1mFound solution: 2023625[0m c ---[ 0]---> Sorter-cost: 4272 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 | 625 | 58090 138077 | 19363 570 15593 27.4 | 10.581 % | c ============================================================================== c [1mFound solution: 1879337[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 674 | 58126 138234 | 19375 619 16889 27.3 | 10.581 % | c ============================================================================== c [1mFound solution: 1869737[0m c ---[ 0]---> Sorter-cost: 2313 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 | 769 | 44561 107019 | 14853 599 17347 29.0 | 10.581 % | c ============================================================================== c [1mFound solution: 1867930[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 849 | 44286 106449 | 14762 671 18131 27.0 | 10.581 % | c ============================================================================== c [1mFound solution: 1867929[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 888 | 44096 106009 | 14698 709 18897 26.7 | 10.581 % | c ============================================================================== c [1mFound solution: 1861529[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 931 | 44001 105801 | 14667 751 19547 26.0 | 10.581 % | c | 1031 | 44001 105801 | 16133 851 21225 24.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1856377[0m c ---[ 0]---> Sorter-cost: 11 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 | 1180 | 44013 105832 | 14671 1000 24129 24.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1856025[0m c ---[ 0]---> Sorter-cost: 11 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 | 1232 | 44025 105861 | 14675 1052 25381 24.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1856024[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1267 | 44040 105898 | 14680 1087 25930 23.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1856017[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1282 | 43972 105752 | 14657 1098 26006 23.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1856015[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1283 | 43989 105792 | 14663 1099 26008 23.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1856013[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1287 | 44007 105834 | 14669 1103 26028 23.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1856012[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1293 | 44025 105876 | 14675 1109 26171 23.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1856004[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1297 | 44043 105918 | 14681 1113 26181 23.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1856003[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1305 | 44058 105953 | 14686 1121 26239 23.4 | 32.357 % | c ============================================================================== c [1mFound solution: 1856001[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1306 | 44073 105988 | 14691 1122 26252 23.4 | 32.357 % | c ============================================================================== c [1mFound solution: 1856000[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1310 | 44084 106015 | 14694 1126 26318 23.4 | 32.357 % | c ============================================================================== c [1mFound solution: 1849309[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1341 | 44045 105935 | 14681 1156 26690 23.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1849260[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1402 | 44055 105963 | 14685 1217 27660 22.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1848844[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 | 1476 | 44029 105909 | 14676 1289 29035 22.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1848317[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1497 | 44029 105912 | 14676 1307 29140 22.3 | 32.357 % | c ============================================================================== c [1mFound solution: 1848316[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1528 | 44043 105944 | 14681 1338 29508 22.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1848315[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 | 1567 | 44050 105961 | 14683 1377 30108 21.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1848236[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 | 1588 | 43975 105795 | 14658 1396 30461 21.8 | 32.357 % | c ============================================================================== c [1mFound solution: 1847220[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1687 | 43988 105829 | 14662 1495 31811 21.3 | 32.357 % | c ============================================================================== c [1mFound solution: 1847219[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1689 | 44001 105863 | 14667 1497 31818 21.3 | 32.357 % | c ============================================================================== c [1mFound solution: 1847156[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1694 | 44014 105895 | 14671 1502 31836 21.2 | 32.357 % | c ============================================================================== c [1mFound solution: 1847155[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1703 | 44027 105927 | 14675 1511 31895 21.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1847153[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1709 | 44040 105960 | 14680 1517 31953 21.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1847028[0m c ---[ 0]---> Sorter-cost: 11 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 | 1714 | 44053 105991 | 14684 1522 32049 21.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1846772[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1731 | 44066 106021 | 14688 1539 32311 21.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1846771[0m c ---[ 0]---> Sorter-cost: 11 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 | 1731 | 44079 106052 | 14693 1539 32311 21.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1846769[0m c ---[ 0]---> Sorter-cost: 11 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 | 1731 | 44092 106083 | 14697 1539 32311 21.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1846768[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1731 | 44107 106121 | 14702 1539 32311 21.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1846767[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1734 | 44120 106154 | 14706 1542 32333 21.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1846696[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1738 | 44139 106199 | 14713 1546 32351 20.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1846695[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1742 | 44158 106244 | 14719 1550 32363 20.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1846692[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1743 | 44176 106286 | 14725 1551 32367 20.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1846520[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1748 | 44190 106320 | 14730 1556 32438 20.8 | 32.357 % | c ============================================================================== c [1mFound solution: 1846496[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1752 | 44206 106358 | 14735 1560 32479 20.8 | 32.357 % | c ============================================================================== c [1mFound solution: 1846488[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1770 | 44222 106395 | 14740 1578 32676 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846048[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1784 | 44237 106430 | 14745 1592 32971 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846040[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1785 | 44251 106462 | 14750 1593 32975 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846039[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1785 | 44267 106499 | 14755 1593 32975 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846036[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1785 | 44283 106536 | 14761 1593 32975 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846035[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1786 | 44299 106573 | 14766 1594 32979 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846033[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1786 | 44314 106607 | 14771 1594 32979 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846032[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1786 | 44330 106644 | 14776 1594 32979 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846012[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1789 | 44346 106680 | 14782 1597 32997 20.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1846008[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1792 | 44359 106709 | 14786 1600 33015 20.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1845988[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1798 | 44373 106742 | 14791 1606 33029 20.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1845928[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1798 | 44387 106774 | 14795 1606 33029 20.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1845924[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1798 | 44401 106806 | 14800 1606 33029 20.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1845923[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1802 | 44420 106849 | 14806 1610 33059 20.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1845920[0m c ---[ 0]---> Sorter-cost: 11 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 | 1818 | 44436 106885 | 14812 1626 33463 20.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1845914[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1862 | 44433 106878 | 14811 1669 34185 20.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1845912[0m c ---[ 0]---> Sorter-cost: 11 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 | 1865 | 44449 106914 | 14816 1672 34261 20.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1845886[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1877 | 44470 106961 | 14823 1684 34454 20.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1845884[0m c ---[ 0]---> Sorter-cost: 11 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 | 1885 | 44488 107001 | 14829 1692 34485 20.4 | 32.357 % | c ============================================================================== c [1mFound solution: 1845822[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1885 | 44508 107045 | 14836 1692 34485 20.4 | 32.357 % | c ============================================================================== c [1mFound solution: 1845820[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1885 | 44526 107085 | 14842 1692 34485 20.4 | 32.357 % | c ============================================================================== c [1mFound solution: 1845819[0m c ---[ 0]---> Sorter-cost: 11 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 | 1888 | 44540 107116 | 14846 1695 34497 20.4 | 32.357 % | c ============================================================================== c [1mFound solution: 1845798[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1889 | 44561 107163 | 14853 1696 34500 20.3 | 32.357 % | c ============================================================================== c [1mFound solution: 1845790[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1889 | 44580 107205 | 14860 1696 34500 20.3 | 32.357 % | c ============================================================================== c [1mFound solution: 1845788[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1889 | 44598 107245 | 14866 1696 34500 20.3 | 32.357 % | c ============================================================================== c [1mFound solution: 1845782[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1893 | 44615 107283 | 14871 1700 34549 20.3 | 32.357 % | c ============================================================================== c [1mFound solution: 1845779[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1897 | 44628 107312 | 14876 1704 34569 20.3 | 32.357 % | c ============================================================================== c [1mFound solution: 1845770[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1933 | 44646 107353 | 14882 1740 35158 20.2 | 32.357 % | c ============================================================================== c [1mFound solution: 1845763[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 | 1935 | 44655 107373 | 14885 1742 35176 20.2 | 32.357 % | c ============================================================================== c [1mFound solution: 1845762[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1936 | 44674 107415 | 14891 1743 35184 20.2 | 32.357 % | c ============================================================================== c [1mFound solution: 1845760[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 | 1937 | 44683 107435 | 14894 1744 35191 20.2 | 32.357 % | c ============================================================================== c [1mFound solution: 1845722[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1948 | 44697 107468 | 14899 1755 35427 20.2 | 32.357 % | c ============================================================================== c [1mFound solution: 1845720[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1951 | 44709 107495 | 14903 1758 35448 20.2 | 32.357 % | c ============================================================================== c [1mFound solution: 1845658[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1955 | 44721 107522 | 14907 1762 35475 20.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1845656[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1955 | 44733 107549 | 14911 1762 35475 20.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1845651[0m c ---[ 0]---> Sorter-cost: 11 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 | 1957 | 44748 107583 | 14916 1764 35485 20.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1845594[0m c ---[ 0]---> Sorter-cost: 11 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 | 1960 | 44763 107617 | 14921 1767 35500 20.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1845592[0m c ---[ 0]---> Sorter-cost: 11 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 | 1964 | 44778 107651 | 14926 1771 35566 20.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1845562[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1976 | 44794 107687 | 14931 1783 35755 20.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1845560[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1976 | 44810 107723 | 14936 1783 35755 20.1 | 32.357 % | c ============================================================================== c [1mFound solution: 1845530[0m c ---[ 0]---> Sorter-cost: 11 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 | 1977 | 44824 107754 | 14941 1784 35762 20.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1845528[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1977 | 44836 107781 | 14945 1784 35762 20.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1845526[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1990 | 44852 107816 | 14950 1797 35896 20.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1845525[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1991 | 44871 107859 | 14957 1798 35898 20.0 | 32.357 % | c ============================================================================== c [1mFound solution: 1845521[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1994 | 44883 107886 | 14961 1801 35906 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845520[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1995 | 44895 107913 | 14965 1802 35908 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845514[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1997 | 44912 107950 | 14970 1804 35933 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845512[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1999 | 44928 107985 | 14976 1806 35962 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845511[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2001 | 44944 108020 | 14981 1808 35982 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845510[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2001 | 44960 108055 | 14986 1808 35982 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845508[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2001 | 44976 108090 | 14992 1808 35982 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845506[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2003 | 44994 108129 | 14998 1810 36004 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845505[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2003 | 45011 108166 | 15003 1810 36004 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1845504[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2003 | 45023 108193 | 15007 1810 36004 19.9 | 32.357 % | c ============================================================================== c [1mFound solution: 1844783[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2018 | 45036 108224 | 15012 1825 36126 19.8 | 32.357 % | c ============================================================================== c [1mFound solution: 1844656[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2024 | 45050 108258 | 15016 1831 36162 19.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1844640[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2024 | 45061 108284 | 15020 1831 36162 19.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1844528[0m c ---[ 0]---> Sorter-cost: 11 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 | 2027 | 45074 108314 | 15024 1834 36223 19.8 | 32.357 % | c ============================================================================== c [1mFound solution: 1844512[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2033 | 45085 108340 | 15028 1840 36361 19.8 | 32.357 % | c ============================================================================== c [1mFound solution: 1844511[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2043 | 45102 108379 | 15034 1850 36512 19.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1844509[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2047 | 45117 108414 | 15039 1854 36528 19.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1844505[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2050 | 45130 108444 | 15043 1857 36542 19.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1844481[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 | 2055 | 45140 108467 | 15046 1862 36621 19.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1844477[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2058 | 45155 108501 | 15051 1865 36725 19.7 | 32.357 % | c ============================================================================== c [1mFound solution: 1844475[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2087 | 45165 108524 | 15055 1894 37121 19.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1844397[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2093 | 45180 108559 | 15060 1900 37180 19.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1844395[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2093 | 45195 108594 | 15065 1900 37180 19.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1844381[0m c ---[ 0]---> Sorter-cost: 11 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 | 2093 | 45209 108626 | 15069 1900 37180 19.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1844379[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2093 | 45223 108658 | 15074 1900 37180 19.6 | 32.357 % | c ============================================================================== c [1mFound solution: 1844301[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2099 | 45238 108692 | 15079 1906 37226 19.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1844299[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2099 | 45253 108726 | 15084 1906 37226 19.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1844285[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2099 | 45268 108760 | 15089 1906 37226 19.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1844283[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2099 | 45278 108783 | 15092 1906 37226 19.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1844045[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2100 | 45291 108813 | 15097 1907 37230 19.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1844043[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2101 | 45304 108843 | 15101 1908 37234 19.5 | 32.357 % | c ============================================================================== c [1mFound solution: 1844029[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2122 | 45317 108873 | 15105 1929 37648 19.5 | 32.357 % | c | 2222 | 45317 108873 | 16615 2029 39466 19.5 | 32.224 % | c ============================================================================== c [1mFound solution: 1843661[0m c ---[ 0]---> Sorter-cost: 11 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 | 2250 | 45293 108822 | 15097 2054 39778 19.4 | 32.224 % | c ============================================================================== c [1mFound solution: 1843659[0m c ---[ 0]---> Sorter-cost: 11 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 | 2250 | 45305 108850 | 15101 2054 39778 19.4 | 32.224 % | c ============================================================================== c [1mFound solution: 1843645[0m c ---[ 0]---> Sorter-cost: 11 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 | 2250 | 45317 108878 | 15105 2054 39778 19.4 | 32.224 % | c ============================================================================== c [1mFound solution: 1843643[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2250 | 45330 108908 | 15110 2054 39778 19.4 | 32.224 % | c ============================================================================== c [1mFound solution: 1843597[0m c ---[ 0]---> Sorter-cost: 11 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 | 2253 | 45344 108940 | 15114 2057 39791 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843595[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2253 | 45358 108972 | 15119 2057 39791 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843589[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2253 | 45375 109011 | 15125 2057 39791 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843587[0m c ---[ 0]---> Sorter-cost: 11 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 | 2253 | 45390 109045 | 15130 2057 39791 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843585[0m c ---[ 0]---> Sorter-cost: 11 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 | 2253 | 45406 109081 | 15135 2057 39791 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843584[0m c ---[ 0]---> Sorter-cost: 11 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 | 2253 | 45421 109115 | 15140 2057 39791 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843583[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2255 | 45436 109149 | 15145 2059 39801 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843581[0m c ---[ 0]---> Sorter-cost: 11 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 | 2261 | 45450 109181 | 15150 2065 39825 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843547[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2262 | 45465 109215 | 15155 2066 39834 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843378[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2265 | 45483 109256 | 15161 2069 39883 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843355[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 | 2273 | 45493 109278 | 15164 2077 40016 19.3 | 32.224 % | c ============================================================================== c [1mFound solution: 1843323[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2355 | 45505 109304 | 15168 2159 41376 19.2 | 32.224 % | c ============================================================================== c [1mFound solution: 1843291[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2368 | 45517 109330 | 15172 2172 41467 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843259[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 | 2380 | 45527 109352 | 15175 2184 41710 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843227[0m c ---[ 0]---> Sorter-cost: 11 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 | 2380 | 45540 109380 | 15180 2184 41710 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843218[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2380 | 45556 109415 | 15185 2184 41710 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843217[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2381 | 45567 109439 | 15189 2185 41718 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843213[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2381 | 45578 109463 | 15192 2185 41718 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843205[0m c ---[ 0]---> Sorter-cost: 11 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 | 2381 | 45591 109491 | 15197 2185 41718 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843202[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2384 | 45602 109515 | 15200 2188 41736 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843201[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2384 | 45613 109539 | 15204 2188 41736 19.1 | 32.224 % | c ============================================================================== c [1mFound solution: 1843200[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2384 | 45624 109563 | 15208 2188 41736 19.1 | 32.224 % | c ============================================================================== c [1mOptimal solution: 1843200[0m s OPTIMUM FOUND v -STM1_bit_7 -STM1_bit_6 -STM1_bit_5 -STM1_bit_4 -STM1_bit_3 -STM1_bit_2 -STM1_bit_1 -STM1_bit0 -STM1_bit1 STM1_bit2 STM1_bit3 STM1_bit4 STM1_bit5 -STM1_bit6 -STM1_bit7 -STM1_bit8 -STM1_bit9 -STM1_bit10 -STM1_bit11 -STM1_bit12 -ANM1_bit0 ANM1_bit1 ANM1_bit2 -ANM1_bit3 -ANM1_bit4 -UE1_bit_7 -UE1_bit_6 -UE1_bit_5 -UE1_bit_4 -UE1_bit_3 -UE1_bit_2 -UE1_bit_1 -UE1_bit0 -UE1_bit1 -UE1_bit2 -UE1_bit3 -UE1_bit4 -UE1_bit5 -UE1_bit6 -UE1_bit7 -UE1_bit8 -UE1_bit9 -UE1_bit10 -UE1_bit11 -UE1_bit12 STM2_bit0 STM2_bit1 -STM2_bit2 -STM2_bit3 -STM2_bit4 -ANM2_bit0 ANM2_bit1 ANM2_bit2 -ANM2_bit3 -ANM2_bit4 -UE2_bit_7 -UE2_bit_6 -UE2_bit_5 -UE2_bit_4 -UE2_bit_3 -UE2_bit_2 -UE2_bit_1 -UE2_bit0 -UE2_bit1 -UE2_bit2 UE2_bit3 UE2_bit4 -UE2_bit5 UE2_bit6 -UE2_bit7 -UE2_bit8 UE2_bit9 -UE2_bit10 -UE2_bit11 -UE2_bit12 STM3_bit0 STM3_bit1 -STM3_bit2 -STM3_bit3 -STM3_bit4 -ANM3_bit0 -ANM3_bit1 -ANM3_bit2 -ANM3_bit3 ANM3_bit4 -UE3_bit_7 -UE3_bit_6 -UE3_bit_5 -UE3_bit_4 -UE3_bit_3 -UE3_bit_2 -UE3_bit_1 -UE3_bit0 -UE3_bit1 -UE3_bit2 UE3_bit3 UE3_bit4 -UE3_bit5 UE3_bit6 -UE3_bit7 -UE3_bit8 UE3_bit9 -UE3_bit10 -UE3_bit11 -UE3_bit12 STM4_bit0 -STM4_bit1 STM4_bit2 STM4_bit3 -STM4_bit4 ANM4_bit0 ANM4_bit1 ANM4_bit2 -ANM4_bit3 -ANM4_bit4 -UE4_bit_7 -UE4_bit_6 -UE4_bit_5 -UE4_bit_4 -UE4_bit_3 -UE4_bit_2 -UE4_bit_1 -UE4_bit0 -UE4_bit1 -UE4_bit2 UE4_bit3 -UE4_bit4 -UE4_bit5 UE4_bit6 UE4_bit7 -UE4_bit8 -UE4_bit9 -UE4_bit10 -UE4_bit11 -UE4_bit12 STM5_bit0 -STM5_bit1 STM5_bit2 STM5_bit3 -STM5_bit4 -ANM5_bit0 -ANM5_bit1 ANM5_bit2 ANM5_bit3 -ANM5_bit4 -UE5_bit_7 -UE5_bit_6 -UE5_bit_5 -UE5_bit_4 -UE5_bit_3 -UE5_bit_2 -UE5_bit_1 -UE5_bit0 -UE5_bit1 -UE5_bit2 -UE5_bit3 -UE5_bit4 -UE5_bit5 -UE5_bit6 -UE5_bit7 -UE5_bit8 -UE5_bit9 -UE5_bit10 -UE5_bit11 -UE5_bit12 -STM6_bit0 STM6_bit1 -STM6_bit2 -STM6_bit3 STM6_bit4 -ANM6_bit0 -ANM6_bit1 -ANM6_bit2 -ANM6_bit3 -ANM6_bit4 -UE6_bit_7 -UE6_bit_6 -UE6_bit_5 -UE6_bit_4 -UE6_bit_3 -UE6_bit_2 -UE6_bit_1 -UE6_bit0 UE6_bit1 UE6_bit2 UE6_bit3 -UE6_bit4 UE6_bit5 UE6_bit6 UE6_bit7 -UE6_bit8 UE6_bit9 -UE6_bit10 -UE6_bit11 -UE6_bit12 c _______________________________________________________________________________ c c restarts : 155 c conflicts : 2395 (109 /sec) c decisions : 207905 (9453 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 21.9937 s c _______________________________________________________________________________ #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.92 0.98 0.93 2/54 20960 Raw data (stat): 20960 (runsolver) R 20959 22056 22055 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855118760 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0005 s] Raw data (loadavg): 0.93 0.98 0.93 2/55 20964 Raw data (stat): 20960 (minisat+_script) S 20959 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855118760 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0015 s] Raw data (loadavg): 0.94 0.98 0.93 2/55 20964 Raw data (stat): 20960 (minisat+_script) S 20959 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855118760 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+22.1223 s] Raw data (loadavg): 0.94 0.98 0.93 1/53 20964 Raw data (stat): 20960 (minisat+_script) S 20959 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855118760 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 30 Real time (s): 22.1221 CPU time (s): 22.0966 CPU user time (s): 22.0067 CPU system time (s): 0.089986 CPU usage (%): 99.8851 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1843200 #### END VERIFIER DATA ####