Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-flugpl.opb |
MD5SUM | f7c404708fc3042fadfc18ab8efeb9a5 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 14745600 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 265 |
Biggest coefficient in the objective function | 48318382080 |
Number of bits for the biggest coefficient in the objective function | 36 |
Sum of the numbers in the objective function | 103103023008 |
Number of bits of the sum of numbers in the objective function | 37 |
Biggest number in a constraint | 80530636800 |
Number of bits of the biggest number in a constraint | 37 |
Biggest sum of numbers in a constraint | 162146381673 |
Number of bits of the biggest sum of numbers | 38 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 27.8208 |
Number of variables | 265 |
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 | 65 |
LAUNCH ON wulflinc20 THE 2005-09-19 17:47:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2972 boxname=wulflinc20 idbench=628 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f7c404708fc3042fadfc18ab8efeb9a5 /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-flugpl.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-flugpl.opb IDLAUNCH: 2972 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 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: 878684 kB Buffers: 40524 kB Cached: 84648 kB SwapCached: 832 kB Active: 71064 kB Inactive: 56744 kB HighTotal: 131008 kB HighFree: 43120 kB LowTotal: 903652 kB LowFree: 835564 kB SwapTotal: 2097892 kB SwapFree: 2096604 kB Dirty: 52 kB Writeback: 0 kB Mapped: 5736 kB Slab: 22564 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 17:47:42 (client local time) WITH STATUS 30 IN 37.1164 SECONDS stats: 2972 0 37.1164 30
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]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 9]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 8]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 7]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 6]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 5]---> BDD-cost: 20 c ---[ 4]---> BDD-cost: 89 c ---[ 3]---> BDD-cost: 89 c ---[ 2]---> BDD-cost: 89 c ---[ 1]---> BDD-cost: 89 c ---[ 0]---> BDD-cost: 89 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 8288 19783 | 2762 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 16054272[0m c ---[ 0]---> Sorter-cost: 9301 Base: 2 2 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 | 43 | 31968 75043 | 10656 43 241 5.6 | 0.000 % | c ============================================================================== c [1mFound solution: 16051230[0m c ---[ 0]---> Sorter-cost: 6121 Base: 2 2 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 | 117 | 46354 108670 | 15451 115 2476 21.5 | 0.000 % | c | 217 | 46019 107919 | 16996 208 3066 14.7 | 2.333 % | c ============================================================================== c [1mFound solution: 16040959[0m c ---[ 0]---> Sorter-cost: 4638 Base: 2 2 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 | 326 | 56576 132606 | 18858 308 4436 14.4 | 2.333 % | c ============================================================================== c [1mFound solution: 16040956[0m c ---[ 0]---> Sorter-cost: 5638 Base: 2 2 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 | 66435 155830 | 22145 346 5317 15.4 | 2.333 % | c ============================================================================== c [1mFound solution: 15803900[0m c ---[ 0]---> Sorter-cost: 4729 Base: 2 2 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 | 415 | 70525 165737 | 23508 295 5059 17.1 | 2.333 % | c ============================================================================== c [1mFound solution: 15803575[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 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 | 428 | 70207 165064 | 23402 304 5100 16.8 | 2.333 % | c ============================================================================== c [1mFound solution: 15542010[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 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 | 432 | 70224 165109 | 23408 308 5192 16.9 | 2.333 % | c ============================================================================== c [1mFound solution: 15410911[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 438 | 70243 165154 | 23414 314 5370 17.1 | 2.333 % | c ============================================================================== c [1mFound solution: 15328990[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 536 | 70183 165036 | 23394 410 7122 17.4 | 2.333 % | c ============================================================================== c [1mFound solution: 15317983[0m c ---[ 0]---> Sorter-cost: 2314 Base: 2 2 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 | 576 | 51566 122353 | 17188 390 7076 18.1 | 2.333 % | c ============================================================================== c [1mFound solution: 15317951[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 583 | 51594 122465 | 17198 397 7107 17.9 | 2.333 % | c ============================================================================== c [1mFound solution: 15317947[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 583 | 51604 122494 | 17201 397 7107 17.9 | 2.333 % | c ============================================================================== c [1mFound solution: 15317943[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 583 | 51614 122522 | 17204 397 7107 17.9 | 2.333 % | c ============================================================================== c [1mFound solution: 15317941[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 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 | 584 | 51629 122564 | 17209 398 7111 17.9 | 2.333 % | c ============================================================================== c [1mFound solution: 15317939[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 591 | 51642 122601 | 17214 405 7162 17.7 | 2.333 % | c ============================================================================== c [1mFound solution: 15317910[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 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 | 600 | 51658 122644 | 17219 414 7234 17.5 | 2.333 % | c ============================================================================== c [1mFound solution: 15266710[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 625 | 51433 122122 | 17144 435 7579 17.4 | 2.333 % | c ============================================================================== c [1mFound solution: 15131542[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 692 | 51387 122020 | 17129 499 8510 17.1 | 2.333 % | c ============================================================================== c [1mFound solution: 14859670[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 748 | 51392 122040 | 17130 553 9143 16.5 | 2.333 % | c | 848 | 51355 121954 | 18843 648 12068 18.6 | 36.570 % | c ============================================================================== c [1mFound solution: 14859669[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 935 | 51148 121507 | 17049 702 12843 18.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14859654[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 941 | 51162 121546 | 17054 708 12921 18.2 | 36.570 % | c ============================================================================== c [1mFound solution: 14859606[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 992 | 51176 121584 | 17058 759 13860 18.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14858646[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 993 | 51184 121607 | 17061 760 13871 18.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14858645[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 1005 | 51192 121630 | 17064 772 14036 18.2 | 36.570 % | c ============================================================================== c [1mFound solution: 14858644[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 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 | 1009 | 51208 121673 | 17069 776 14103 18.2 | 36.570 % | c ============================================================================== c [1mFound solution: 14858638[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 1017 | 51224 121715 | 17074 784 14284 18.2 | 36.570 % | c ============================================================================== c [1mFound solution: 14858625[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 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 | 1086 | 51171 121604 | 17057 850 15185 17.9 | 36.570 % | c ============================================================================== c [1mFound solution: 14858370[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 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 | 1115 | 51183 121637 | 17061 878 15426 17.6 | 36.570 % | c ============================================================================== c [1mFound solution: 14858369[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 1134 | 51194 121667 | 17064 897 15740 17.5 | 36.570 % | c ============================================================================== c [1mFound solution: 14858354[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 1169 | 51171 121622 | 17057 931 16186 17.4 | 36.570 % | c ============================================================================== c [1mFound solution: 14858353[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 1187 | 51185 121660 | 17061 949 16435 17.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14858322[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 1190 | 51200 121699 | 17066 952 16534 17.4 | 36.570 % | c ============================================================================== c [1mFound solution: 14858321[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 1190 | 51215 121738 | 17071 952 16534 17.4 | 36.570 % | c ============================================================================== c [1mFound solution: 14858320[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 1190 | 51232 121781 | 17077 952 16534 17.4 | 36.570 % | c ============================================================================== c [1mFound solution: 14858312[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 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 | 1194 | 51248 121822 | 17082 956 16562 17.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14857672[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 1195 | 51260 121855 | 17086 957 16567 17.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14856648[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 1196 | 51269 121879 | 17089 958 16574 17.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14856392[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 1200 | 51100 121488 | 17033 961 16602 17.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14856264[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 1200 | 51108 121510 | 17036 961 16602 17.3 | 36.570 % | c ============================================================================== c [1mFound solution: 14850888[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 1287 | 51122 121546 | 17040 1048 18139 17.3 | 36.570 % | c | 1391 | 51122 121546 | 18744 1152 20103 17.5 | 36.981 % | c ============================================================================== c [1mFound solution: 14850632[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 1432 | 51054 121398 | 17018 1190 20841 17.5 | 36.981 % | c ============================================================================== c [1mFound solution: 14849672[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 1454 | 51071 121440 | 17023 1212 21234 17.5 | 36.981 % | c ============================================================================== c [1mFound solution: 14849669[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 1458 | 51091 121489 | 17030 1216 21313 17.5 | 36.981 % | c ============================================================================== c [1mFound solution: 14849416[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 1467 | 51106 121526 | 17035 1225 21479 17.5 | 36.981 % | c ============================================================================== c [1mFound solution: 14849411[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 1482 | 51125 121572 | 17041 1240 21533 17.4 | 36.981 % | c ============================================================================== c [1mFound solution: 14848933[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 1492 | 51143 121617 | 17047 1250 21572 17.3 | 36.981 % | c ============================================================================== c [1mFound solution: 14848902[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 1493 | 51156 121649 | 17052 1251 21577 17.2 | 36.981 % | c ============================================================================== c [1mFound solution: 14848518[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 1496 | 51172 121687 | 17057 1254 21584 17.2 | 36.981 % | c ============================================================================== c [1mFound solution: 14848517[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 1496 | 51188 121725 | 17062 1254 21584 17.2 | 36.981 % | c ============================================================================== c [1mFound solution: 14848516[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 1496 | 51208 121772 | 17069 1254 21584 17.2 | 36.981 % | c ============================================================================== c [1mFound solution: 14847493[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 1497 | 51218 121798 | 17072 1255 21591 17.2 | 36.981 % | c ============================================================================== c [1mFound solution: 14846469[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 1497 | 51230 121827 | 17076 1255 21591 17.2 | 36.981 % | c ============================================================================== c [1mFound solution: 14846468[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 1497 | 51242 121856 | 17080 1255 21591 17.2 | 36.981 % | c ============================================================================== c [1mFound solution: 14830078[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 1586 | 51261 121899 | 17087 1344 23063 17.2 | 36.981 % | c ============================================================================== c [1mFound solution: 14827082[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 1631 | 51278 121943 | 17092 1389 24305 17.5 | 36.981 % | c ============================================================================== c [1mFound solution: 14794363[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 1653 | 51287 121969 | 17095 1411 24530 17.4 | 36.981 % | c | 1754 | 51203 121775 | 18804 1510 26470 17.5 | 37.038 % | c ============================================================================== c [1mFound solution: 14794308[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 1770 | 51217 121812 | 17072 1526 26747 17.5 | 37.038 % | c ============================================================================== c [1mFound solution: 14794267[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 1770 | 51228 121842 | 17076 1526 26747 17.5 | 37.038 % | c ============================================================================== c [1mFound solution: 14794076[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 1770 | 51244 121884 | 17081 1526 26747 17.5 | 37.038 % | c ============================================================================== c [1mFound solution: 14794012[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 1771 | 51258 121921 | 17086 1527 26751 17.5 | 37.038 % | c ============================================================================== c [1mFound solution: 14793563[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 1771 | 51271 121956 | 17090 1527 26751 17.5 | 37.038 % | c ============================================================================== c [1mFound solution: 14793500[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 1771 | 51281 121983 | 17093 1527 26751 17.5 | 37.038 % | c | 1871 | 51281 121983 | 18802 1627 28463 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14792548[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 1966 | 51296 122023 | 17098 1722 30026 17.4 | 37.014 % | c ============================================================================== c [1mFound solution: 14792475[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 1970 | 51309 122057 | 17103 1726 30155 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14790492[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 1978 | 51319 122084 | 17106 1734 30397 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14790427[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2002 | 51329 122109 | 17109 1758 30962 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14790243[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2004 | 51345 122150 | 17115 1760 30991 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14777116[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 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 | 2058 | 51355 122175 | 17118 1814 31984 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14777091[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2058 | 51370 122212 | 17123 1814 31984 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14777084[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2058 | 51387 122253 | 17129 1814 31984 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14777083[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2061 | 51400 122285 | 17133 1817 31998 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776859[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2061 | 51413 122317 | 17137 1817 31998 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776835[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2061 | 51428 122353 | 17142 1817 31998 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776827[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2061 | 51440 122382 | 17146 1817 31998 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776603[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2061 | 51454 122416 | 17151 1817 31998 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776579[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2061 | 51468 122450 | 17156 1817 31998 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776571[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2061 | 51481 122481 | 17160 1817 31998 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776515[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2063 | 51498 122522 | 17166 1819 32003 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776507[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2065 | 51470 122460 | 17156 1820 32005 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776483[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2065 | 51488 122503 | 17162 1820 32005 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776451[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2065 | 51503 122539 | 17167 1820 32005 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776443[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2065 | 51516 122570 | 17172 1820 32005 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776419[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2070 | 51529 122601 | 17176 1825 32022 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14776415[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2076 | 51545 122640 | 17181 1831 32259 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776413[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 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 | 2089 | 51564 122685 | 17188 1844 32471 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776412[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2091 | 51578 122718 | 17192 1846 32495 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776411[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2092 | 51592 122751 | 17197 1847 32505 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776403[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2092 | 51611 122796 | 17203 1847 32505 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776395[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2092 | 51629 122838 | 17209 1847 32505 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776387[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2093 | 51645 122876 | 17215 1848 32518 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776371[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2096 | 51660 122911 | 17220 1851 32599 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776363[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2096 | 51677 122951 | 17225 1851 32599 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776362[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2100 | 51696 122995 | 17232 1855 32627 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776361[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 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 | 2102 | 51716 123042 | 17238 1857 32649 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776360[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2102 | 51735 123086 | 17245 1857 32649 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776357[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2102 | 51750 123121 | 17250 1857 32649 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14776356[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2102 | 51767 123161 | 17255 1857 32649 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14774855[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 2111 | 51789 123212 | 17263 1866 32746 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14773063[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2134 | 51807 123254 | 17269 1889 33202 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14770247[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2151 | 51822 123287 | 17274 1906 33641 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14766151[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2158 | 51837 123320 | 17279 1913 33842 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14766147[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2165 | 51669 122930 | 17223 1918 33978 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14766119[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2167 | 51690 122976 | 17230 1920 33998 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14766118[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2170 | 51711 123022 | 17237 1923 34008 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14762021[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2183 | 51723 123048 | 17241 1936 34155 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14762020[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2184 | 51735 123074 | 17245 1937 34163 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14762019[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2187 | 51751 123108 | 17250 1940 34175 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14761992[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2188 | 51767 123142 | 17255 1941 34180 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14761988[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2189 | 51781 123172 | 17260 1942 34186 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14761985[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2190 | 51797 123206 | 17265 1943 34192 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14761984[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2229 | 51817 123248 | 17272 1982 34913 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14759432[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2235 | 51831 123282 | 17277 1988 35030 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14758920[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2236 | 51844 123313 | 17281 1989 35067 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14758916[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2236 | 51857 123344 | 17285 1989 35067 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14758913[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2236 | 51872 123379 | 17290 1989 35067 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14758912[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2236 | 51890 123420 | 17296 1989 35067 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14758908[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2237 | 51900 123444 | 17300 1990 35072 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14758664[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2238 | 51914 123478 | 17304 1991 35077 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14758408[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2241 | 51926 123507 | 17308 1994 35096 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14758184[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2281 | 51798 123213 | 17266 2027 35424 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14758180[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2281 | 51814 123250 | 17271 2027 35424 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14758179[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2281 | 51829 123285 | 17276 2027 35424 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14758178[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2281 | 51848 123329 | 17282 2027 35424 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14758177[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2281 | 51867 123373 | 17289 2027 35424 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14758176[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2281 | 51886 123417 | 17295 2027 35424 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14758172[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2282 | 51897 123443 | 17299 2028 35427 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14757672[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2282 | 51908 123471 | 17302 2028 35427 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14757160[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2282 | 51921 123502 | 17307 2028 35427 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14757156[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2282 | 51934 123533 | 17311 2028 35427 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14757155[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2282 | 51947 123564 | 17315 2028 35427 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14757128[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2282 | 51961 123598 | 17320 2028 35427 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14757124[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2282 | 51978 123638 | 17326 2028 35427 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14757123[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2282 | 51991 123669 | 17330 2028 35427 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14756648[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2284 | 52005 123702 | 17335 2030 35447 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14754600[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2288 | 52016 123727 | 17338 2034 35608 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14754596[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2300 | 52029 123757 | 17343 2046 35877 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14754595[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2301 | 52042 123787 | 17347 2047 35892 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14754344[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2301 | 52057 123821 | 17352 2047 35892 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14754340[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2301 | 52072 123855 | 17357 2047 35892 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14754339[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2301 | 52087 123889 | 17362 2047 35892 17.5 | 37.014 % | c ============================================================================== c [1mFound solution: 14753576[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2371 | 52098 123914 | 17366 2117 37650 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753572[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2378 | 52109 123941 | 17369 2124 37798 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753571[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2391 | 52087 123893 | 17362 2136 37996 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753320[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2394 | 52098 123920 | 17366 2139 38048 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753316[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2401 | 52109 123947 | 17369 2146 38254 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753315[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2420 | 52120 123974 | 17373 2165 38618 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753288[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2421 | 52131 124000 | 17377 2166 38627 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753284[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2421 | 52142 124027 | 17380 2166 38627 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753283[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2421 | 52153 124054 | 17384 2166 38627 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753282[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2421 | 52167 124088 | 17389 2166 38627 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753281[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2421 | 52181 124122 | 17393 2166 38627 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753280[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2421 | 52197 124160 | 17399 2166 38627 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753276[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2421 | 52208 124186 | 17402 2166 38627 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753275[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2422 | 52219 124213 | 17406 2167 38632 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753060[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2422 | 52230 124238 | 17410 2167 38632 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753032[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2422 | 52241 124263 | 17413 2167 38632 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753028[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2422 | 52252 124288 | 17417 2167 38632 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753024[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2465 | 52229 124237 | 17409 2208 39214 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14753020[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2468 | 52243 124271 | 17414 2211 39323 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14752296[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2474 | 52256 124301 | 17418 2217 39408 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14751780[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 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 | 2475 | 52267 124327 | 17422 2218 39411 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14751752[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2476 | 52280 124357 | 17426 2219 39413 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14751748[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2476 | 52293 124387 | 17431 2219 39413 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14751744[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2476 | 52304 124413 | 17434 2219 39413 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14751740[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2477 | 52317 124443 | 17439 2220 39415 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14751739[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2477 | 52328 124468 | 17442 2220 39415 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14750696[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2490 | 52343 124505 | 17447 2233 39972 17.9 | 37.014 % | c ============================================================================== c [1mFound solution: 14750568[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2497 | 52361 124547 | 17453 2240 40106 17.9 | 37.014 % | c ============================================================================== c [1mFound solution: 14749796[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2501 | 52377 124582 | 17459 2244 40209 17.9 | 37.014 % | c ============================================================================== c [1mFound solution: 14749764[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2505 | 52392 124615 | 17464 2248 40295 17.9 | 37.014 % | c ============================================================================== c [1mFound solution: 14749760[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2505 | 52412 124659 | 17470 2248 40295 17.9 | 37.014 % | c ============================================================================== c [1mFound solution: 14749756[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2505 | 52432 124703 | 17477 2248 40295 17.9 | 37.014 % | c ============================================================================== c [1mFound solution: 14749728[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2510 | 52448 124738 | 17482 2253 40306 17.9 | 37.014 % | c ============================================================================== c [1mFound solution: 14749720[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 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 | 2511 | 52468 124782 | 17489 2254 40310 17.9 | 37.014 % | c ============================================================================== c [1mFound solution: 14749696[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2517 | 52481 124811 | 17493 2260 40331 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14748704[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2521 | 52496 124845 | 17498 2264 40342 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14748700[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2522 | 52511 124879 | 17503 2265 40345 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14748699[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2525 | 52525 124911 | 17508 2268 40383 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14748688[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2531 | 52542 124949 | 17514 2274 40411 17.8 | 37.014 % | c ============================================================================== c [1mFound solution: 14748676[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2535 | 52554 124976 | 17518 2278 40426 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14748672[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2537 | 52566 125003 | 17522 2280 40437 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14748668[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2543 | 52578 125030 | 17526 2286 40455 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14748667[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2555 | 52590 125057 | 17530 2298 40625 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14748553[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2564 | 52608 125099 | 17536 2307 40738 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14747785[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2566 | 52625 125137 | 17541 2309 40763 17.7 | 37.014 % | c ============================================================================== c [1mFound solution: 14747781[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2567 | 52640 125170 | 17546 2310 40765 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14747273[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2568 | 52655 125204 | 17551 2311 40769 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14747269[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2568 | 52666 125228 | 17555 2311 40769 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14747268[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2568 | 52684 125269 | 17561 2311 40769 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14747017[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2568 | 52700 125305 | 17566 2311 40769 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14747013[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2568 | 52716 125341 | 17572 2311 40769 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14747012[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2568 | 52732 125377 | 17577 2311 40769 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14746949[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2570 | 52753 125424 | 17584 2313 40784 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14746943[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2572 | 52772 125467 | 17590 2315 40794 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14746881[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2573 | 52790 125507 | 17596 2316 40799 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14746877[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 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 | 2574 | 52810 125551 | 17603 2317 40805 17.6 | 37.014 % | c ============================================================================== c [1mFound solution: 14746369[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2577 | 52824 125582 | 17608 2320 40844 17.6 | 37.014 % | c | 2677 | 52804 125535 | 19368 2418 42373 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746368[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2679 | 52818 125566 | 17606 2420 42420 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746365[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2679 | 52832 125597 | 17610 2420 42420 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746241[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2679 | 52848 125632 | 17616 2420 42420 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746209[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2680 | 52866 125672 | 17622 2421 42425 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746177[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2681 | 52886 125716 | 17628 2422 42429 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746153[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2682 | 52904 125755 | 17634 2423 42439 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746145[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2685 | 52920 125790 | 17640 2426 42445 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746113[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2686 | 52934 125821 | 17644 2427 42452 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14746112[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2686 | 52948 125852 | 17649 2427 42452 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745889[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2690 | 52959 125876 | 17653 2431 42566 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745888[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2691 | 52970 125900 | 17656 2432 42573 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745885[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2691 | 52989 125942 | 17663 2432 42573 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745884[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 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 | 2692 | 53000 125966 | 17666 2433 42578 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745883[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2692 | 53012 125992 | 17670 2433 42578 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745865[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2692 | 53029 126029 | 17676 2433 42578 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745864[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 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 | 2693 | 53042 126057 | 17680 2434 42585 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745761[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2695 | 53060 126096 | 17686 2436 42601 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745705[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2697 | 53077 126133 | 17692 2438 42611 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745697[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2699 | 53091 126163 | 17697 2440 42622 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745673[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2699 | 53110 126204 | 17703 2440 42622 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745665[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2700 | 53124 126234 | 17708 2441 42632 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745661[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2702 | 53143 126275 | 17714 2443 42651 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745641[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 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 | 2702 | 53155 126301 | 17718 2443 42651 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745633[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2703 | 53169 126331 | 17723 2444 42661 17.5 | 36.944 % | c ============================================================================== c [1mFound solution: 14745629[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 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 | 2706 | 53184 126363 | 17728 2447 42686 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745621[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 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 | 2708 | 53200 126397 | 17733 2449 42693 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745610[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2710 | 53217 126433 | 17739 2451 42731 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745608[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 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 | 2711 | 53229 126459 | 17743 2452 42737 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745607[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 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 | 2712 | 53246 126495 | 17748 2453 42746 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745606[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2713 | 53260 126525 | 17753 2454 42751 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745605[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2716 | 53274 126555 | 17758 2457 42770 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745603[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2747 | 53288 126585 | 17762 2488 43194 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745602[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 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 | 2747 | 53302 126615 | 17767 2488 43194 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745601[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 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 | 2747 | 53315 126643 | 17771 2488 43194 17.4 | 36.944 % | c ============================================================================== c [1mFound solution: 14745600[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 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 | 2747 | 53326 126667 | 17775 2488 43194 17.4 | 36.944 % | c ============================================================================== c [1mOptimal solution: 14745600[0m s OPTIMUM FOUND v -STM1_bit_10 -STM1_bit_9 -STM1_bit_8 -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 -STM1_bit13 -STM1_bit14 -STM1_bit15 -STM1_bit16 -STM1_bit17 -STM1_bit18 -STM1_bit19 -ANM1_bit0 ANM1_bit1 ANM1_bit2 -ANM1_bit3 -ANM1_bit4 -UE1_bit_10 -UE1_bit_9 -UE1_bit_8 -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 -UE1_bit13 -UE1_bit14 -UE1_bit15 -UE1_bit16 -UE1_bit17 -UE1_bit18 -UE1_bit19 STM2_bit0 STM2_bit1 -STM2_bit2 -STM2_bit3 -STM2_bit4 -ANM2_bit0 ANM2_bit1 ANM2_bit2 -ANM2_bit3 -ANM2_bit4 -UE2_bit_10 -UE2_bit_9 -UE2_bit_8 -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 -UE2_bit13 -UE2_bit14 -UE2_bit15 -UE2_bit16 -UE2_bit17 -UE2_bit18 -UE2_bit19 STM3_bit0 STM3_bit1 -STM3_bit2 -STM3_bit3 -STM3_bit4 -ANM3_bit0 -ANM3_bit1 -ANM3_bit2 -ANM3_bit3 ANM3_bit4 -UE3_bit_10 -UE3_bit_9 -UE3_bit_8 -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 -UE3_bit13 -UE3_bit14 -UE3_bit15 -UE3_bit16 -UE3_bit17 -UE3_bit18 -UE3_bit19 STM4_bit0 -STM4_bit1 STM4_bit2 STM4_bit3 -STM4_bit4 ANM4_bit0 ANM4_bit1 ANM4_bit2 -ANM4_bit3 -ANM4_bit4 -UE4_bit_10 -UE4_bit_9 -UE4_bit_8 -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 -UE4_bit13 -UE4_bit14 -UE4_bit15 -UE4_bit16 -UE4_bit17 -UE4_bit18 -UE4_bit19 STM5_bit0 -STM5_bit1 STM5_bit2 STM5_bit3 -STM5_bit4 -ANM5_bit0 -ANM5_bit1 ANM5_bit2 ANM5_bit3 -ANM5_bit4 -UE5_bit_10 -UE5_bit_9 -UE5_bit_8 -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 -UE5_bit13 -UE5_bit14 -UE5_bit15 -UE5_bit16 -UE5_bit17 -UE5_bit18 -UE5_bit19 -STM6_bit0 STM6_bit1 -STM6_bit2 -STM6_bit3 STM6_bit4 -ANM6_bit0 -ANM6_bit1 -ANM6_bit2 -ANM6_bit3 -ANM6_bit4 -UE6_bit_10 -UE6_bit_9 -UE6_bit_8 -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 -UE6_bit13 -UE6_bit14 -UE6_bit15 -UE6_bit16 -UE6_bit17 -UE6_bit18 -UE6_bit19 c _______________________________________________________________________________ c c restarts : 239 c conflicts : 2799 (76 /sec) c decisions : 242915 (6582 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 36.9074 s c _______________________________________________________________________________
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/22597/stat): 22597 (minisat+_script) R 22596 22597 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851809276 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/22597/statm): 174 3 169 147 0 27 0 [pid=22597] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=22598 New process pid=22599 New process pid=22600 execve syscall for /bin/sed executable One traced child (pid=22599) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=22600) exited with status: 0 One traced child (pid=22598) exited with status: 0 New process pid=22601 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-flugpl.opb [startup+10.0043 s] Raw data (loadavg): 0.94 0.97 0.73 2/57 22601 Raw data (/proc/22597/stat): 22597 (minisat+_script) S 22596 22597 2660 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851809276 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22597/statm): 531 226 485 147 0 384 0 [pid=22597] vsize: 2124 Raw data (/proc/22601/stat): 22601 (minisat+_64-bit) R 22597 22597 2660 0 -1 0 2712 0 2 0 968 13 0 0 25 0 1 0 1851809281 12140544 2649 4294967295 134512640 135094434 3221224432 3221223100 134550364 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22601/statm): 2964 2649 145 145 0 2819 0 [pid=22601] vsize: 11856 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 13980 [startup+20.0049 s] Raw data (loadavg): 0.95 0.97 0.73 2/57 22601 Raw data (/proc/22597/stat): 22597 (minisat+_script) S 22596 22597 2660 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851809276 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22597/statm): 531 226 485 147 0 384 0 [pid=22597] vsize: 2124 Raw data (/proc/22601/stat): 22601 (minisat+_64-bit) R 22597 22597 2660 0 -1 0 2903 0 2 0 1966 15 0 0 25 0 1 0 1851809281 14565376 2840 4294967295 134512640 135094434 3221224432 3221222160 134676595 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22601/statm): 3556 2840 145 145 0 3411 0 [pid=22601] vsize: 14224 Current children cumulated CPU time (s) 19.83 Current children cumulated vsize (Kb) 16348 [startup+30.0057 s] Raw data (loadavg): 0.95 0.97 0.73 2/57 22601 Raw data (/proc/22597/stat): 22597 (minisat+_script) S 22596 22597 2660 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851809276 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22597/statm): 531 226 485 147 0 384 0 [pid=22597] vsize: 2124 Raw data (/proc/22601/stat): 22601 (minisat+_64-bit) R 22597 22597 2660 0 -1 0 2912 0 2 0 2965 15 0 0 25 0 1 0 1851809281 14565376 2849 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22601/statm): 3556 2849 145 145 0 3411 0 [pid=22601] vsize: 14224 Current children cumulated CPU time (s) 29.82 Current children cumulated vsize (Kb) 16348 One traced child (pid=22601) exited with status: 30 One traced child (pid=22597) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 37.2921 CPU time (s): 37.1164 CPU user time (s): 36.9244 CPU system time (s): 0.19197 CPU usage (%): 99.5287 Max. virtual memory (cumulated for all children) (Kb): 16348
Verifier: OK 14745600