Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-lseu.opb |
MD5SUM | 99657262afbbfce7034a3ec6b29d9b3b |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1120 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 85 |
Biggest coefficient in the objective function | 517 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 15494 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 1656 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 15494 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02984 |
Number of variables | 89 |
Total number of constraints | 117 |
Number of constraints which are clauses | 2 |
Number of constraints which are cardinality constraints (but not clauses) | 104 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 47 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc18 THE 2005-04-21 23:20:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13505 boxname=wulflinc18 idbench=1039 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 99657262afbbfce7034a3ec6b29d9b3b /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-lseu.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-lseu.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-lseu.opb IDLAUNCH: 13505 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 453460 kB Buffers: 26936 kB Cached: 531124 kB SwapCached: 764 kB Active: 167784 kB Inactive: 392292 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 453208 kB SwapTotal: 2097892 kB SwapFree: 2096152 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5100 kB Slab: 15504 kB Committed_AS: 63816 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 23:36:01 (client local time) WITH STATUS 30 IN 903.762 SECONDS stats: 13505 0 903.762 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 28 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): ...s.. c ---[ 28]---> BDD-cost: 3 c ---[ 27]---> BDD-cost: 7 c ---[ 26]---> BDD-cost: 5 c ---[ 24]---> BDD-cost: 3 c ---[ 23]---> BDD-cost: 5 c ---[ 22]---> BDD-cost: 11 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 7 c ---[ 19]---> BDD-cost: 3 c ---[ 18]---> BDD-cost: 7 c ---[ 17]---> BDD-cost: 5 c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> BDD-cost: 5 c ---[ 14]---> BDD-cost: 3 c ---[ 12]---> BDD-cost: 7 c ---[ 9]---> Sorter-cost: 3170 Base: 5 2 2 3 c ---[ 8]---> BDD-cost: 28 c ---[ 7]---> BDD-cost: 202 c ---[ 6]---> Sorter-cost: 1878 Base: 5 2 2 3 c ---[ 4]---> Sorter-cost: 1741 Base: 5 2 2 2 c ---[ 2]---> BDD-cost: 16 c ---[ 0]---> BDD-cost: 32 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 16056 38094 | 4816 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/5893 c -- var.elim.: 2000/5893 c -- var.elim.: 3000/5893 c -- var.elim.: 4000/5893 c -- var.elim.: 5000/5893 c -- var.elim.: 5893/5893 c -- var.elim.: 1000/3116 c -- var.elim.: 2000/3116 c -- var.elim.: 3000/3116 c -- var.elim.: 3116/3116 c -- var.elim.: 87/87 c -- subsuming c -- var.elim.: 917/917 c -- var.elim.: 408/408 c -- subsuming c -- var.elim.: 152/152 c -- var.elim.: 39/39 c | 0 | 13581 44427 | -- 0 -- -- | -- | -2465/6420 c | 0 | 13581 44427 | 5432 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 1.05684 s) c ============================================================================== c [1mFound solution: 2771[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:12453 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 61 | 42740 112584 | 12821 61 3340 54.8 | 0.000 % | c -- subsuming c -- var.elim.: 1000/10532 c -- var.elim.: 2000/10532 c -- var.elim.: 3000/10532 c -- var.elim.: 4000/10532 c -- var.elim.: 5000/10532 c -- var.elim.: 6000/10532 c -- var.elim.: 7000/10532 c -- var.elim.: 8000/10532 c -- var.elim.: 9000/10532 c -- var.elim.: 10000/10532 c -- var.elim.: 10532/10532 c -- var.elim.: 1000/5575 c -- var.elim.: 2000/5575 c -- var.elim.: 3000/5575 c -- var.elim.: 4000/5575 c -- var.elim.: 5000/5575 c -- var.elim.: 5575/5575 c -- var.elim.: 757/757 c -- var.elim.: 288/288 c -- var.elim.: 372/372 c -- var.elim.: 65/65 c -- subsuming c -- var.elim.: 1000/1097 c -- var.elim.: 1097/1097 c -- var.elim.: 652/652 c -- var.elim.: 31/31 c -- var.elim.: 12/12 c -- subsuming c -- var.elim.: 461/461 c -- var.elim.: 110/110 c -- subsuming c -- var.elim.: 61/61 c -- var.elim.: 30/30 c -- var.elim.: 82/82 c -- var.elim.: 31/31 c | 61 | 37322 119614 | -- 61 -- -- | -- | -5307/7293 c | 61 | 37322 119614 | 14928 61 3340 54.8 | 0.000 % | c | 162 | 36805 117593 | 16194 154 5569 36.2 | 3.857 % | c | 312 | 33317 105252 | 16125 254 7355 29.0 | 9.964 % | c | 539 | 33290 105170 | 17723 480 35589 74.1 | 10.024 % | c ============================================================================== c (current CPU-time: 4.40533 s) c ============================================================================== c [1mFound solution: 2760[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 668 | 33836 105851 | 10150 592 40313 68.1 | 10.024 % | c -- subsuming c -- var.elim.: 1000/4245 c -- var.elim.: 2000/4245 c -- var.elim.: 3000/4245 c -- var.elim.: 4000/4245 c -- var.elim.: 4245/4245 c -- var.elim.: 1000/2342 c -- var.elim.: 2000/2342 c -- var.elim.: 2342/2342 c -- var.elim.: 888/888 c -- var.elim.: 613/613 c -- var.elim.: 200/200 c -- subsuming c -- var.elim.: 654/654 c -- var.elim.: 362/362 c -- subsuming c -- var.elim.: 376/376 c -- var.elim.: 21/21 c | 668 | 31864 102975 | -- 592 -- -- | -- | -1935/-2796 c | 668 | 31864 102975 | 12745 360 8120 22.6 | 10.024 % | c | 768 | 30886 99365 | 13589 443 11151 25.2 | 14.617 % | c ============================================================================== c (current CPU-time: 5.78612 s) c ============================================================================== c [1mFound solution: 2728[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 810 | 32423 103353 | 9726 485 11882 24.5 | 14.617 % | c -- subsuming c -- var.elim.: 1000/2476 c -- var.elim.: 2000/2476 c -- var.elim.: 2476/2476 c -- var.elim.: 1000/1428 c -- var.elim.: 1428/1428 c -- var.elim.: 602/602 c -- var.elim.: 447/447 c -- var.elim.: 142/142 c -- subsuming c -- var.elim.: 470/470 c -- var.elim.: 4/4 c -- var.elim.: 4/4 c | 810 | 31101 101245 | -- 485 -- -- | -- | -1301/-2065 c | 810 | 31101 101245 | 12440 469 11575 24.7 | 14.617 % | c ============================================================================== c (current CPU-time: 6.74797 s) c ============================================================================== c [1mFound solution: 2541[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 829 | 31609 102624 | 9482 488 12044 24.7 | 14.617 % | c -- subsuming c -- var.elim.: 749/749 c -- var.elim.: 399/399 c -- var.elim.: 310/310 c -- var.elim.: 201/201 c -- subsuming c -- var.elim.: 169/169 c | 829 | 31123 101502 | -- 488 -- -- | -- | -480/-1109 c | 829 | 31123 101502 | 12449 488 12044 24.7 | 14.617 % | c | 929 | 31123 101502 | 13694 588 17862 30.4 | 14.712 % | c | 1079 | 30916 100824 | 14963 736 20885 28.4 | 15.059 % | c ============================================================================== c (current CPU-time: 7.72083 s) c ============================================================================== c [1mFound solution: 2498[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1234 | 30646 99873 | 9193 883 24002 27.2 | 15.059 % | c -- subsuming c -- var.elim.: 644/644 c -- var.elim.: 422/422 c -- var.elim.: 107/107 c -- var.elim.: 54/54 c -- subsuming c -- var.elim.: 19/19 c -- var.elim.: 5/5 c | 1234 | 30407 99759 | -- 883 -- -- | -- | -238/-111 c | 1234 | 30407 99759 | 12162 768 19979 26.0 | 15.059 % | c | 1334 | 30004 98425 | 13201 857 21780 25.4 | 16.685 % | c | 1485 | 29840 97847 | 14442 1003 30354 30.3 | 16.950 % | c | 1710 | 29827 97785 | 15879 1227 52797 43.0 | 17.022 % | c ============================================================================== c (current CPU-time: 9.1826 s) c ============================================================================== c [1mFound solution: 2481[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1812 | 30366 99114 | 9109 1329 56945 42.8 | 17.022 % | c -- subsuming c -- var.elim.: 1000/1164 c -- var.elim.: 1164/1164 c -- var.elim.: 583/583 c -- var.elim.: 147/147 c -- var.elim.: 1/1 c -- subsuming c -- var.elim.: 85/85 c -- var.elim.: 52/52 c | 1812 | 29936 98642 | -- 1329 -- -- | -- | -412/-435 c | 1812 | 29936 98642 | 11974 1196 43065 36.0 | 17.022 % | c | 1913 | 29896 98502 | 13154 1295 45630 35.2 | 17.169 % | c ============================================================================== c (current CPU-time: 9.82751 s) c ============================================================================== c [1mFound solution: 2477[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1944 | 29829 98253 | 8948 1323 46293 35.0 | 17.169 % | c -- subsuming c -- var.elim.: 274/274 c -- var.elim.: 191/191 c -- var.elim.: 52/52 c -- subsuming c -- var.elim.: 67/67 c | 1944 | 29781 98230 | -- 1323 -- -- | -- | -48/-22 c | 1944 | 29781 98230 | 11912 1293 44828 34.7 | 17.169 % | c | 2045 | 29722 97319 | 13077 1393 49620 35.6 | 17.424 % | c | 2195 | 29665 97129 | 14357 1541 51992 33.7 | 17.532 % | c ============================================================================== c (current CPU-time: 10.7934 s) c ============================================================================== c [1mFound solution: 2438[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2324 | 30279 98682 | 9083 1670 61730 37.0 | 17.532 % | c -- subsuming c -- var.elim.: 1000/1103 c -- var.elim.: 1103/1103 c -- var.elim.: 637/637 c -- var.elim.: 137/137 c -- var.elim.: 29/29 c -- var.elim.: 28/28 c -- subsuming c -- var.elim.: 120/120 c | 2324 | 29813 98499 | -- 1670 -- -- | -- | -451/-152 c | 2324 | 29813 98499 | 11925 1635 55197 33.8 | 17.532 % | c | 2424 | 29523 96696 | 12990 1718 56714 33.0 | 18.045 % | c | 2575 | 28574 93002 | 13829 1854 58224 31.4 | 19.598 % | c | 2800 | 27732 90088 | 14764 2024 62091 30.7 | 21.176 % | c ============================================================================== c (current CPU-time: 12.0012 s) c ============================================================================== c [1mFound solution: 2209[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3009 | 27729 89986 | 8318 2217 67198 30.3 | 21.176 % | c -- subsuming c -- var.elim.: 1000/1712 c -- var.elim.: 1712/1712 c -- var.elim.: 1000/1244 c -- var.elim.: 1244/1244 c -- var.elim.: 407/407 c -- var.elim.: 378/378 c -- subsuming c -- var.elim.: 444/444 c -- var.elim.: 40/40 c | 3009 | 27259 90654 | -- 2217 -- -- | -- | -466/677 c | 3009 | 27259 90654 | 10903 1963 45275 23.1 | 21.176 % | c | 3109 | 27170 90335 | 11954 2062 48761 23.6 | 22.234 % | c | 3259 | 27149 90255 | 13140 2211 58028 26.2 | 22.259 % | c | 3484 | 27149 90255 | 14454 2436 85189 35.0 | 22.259 % | c | 3821 | 26871 89221 | 15736 2766 104440 37.8 | 22.651 % | c ============================================================================== c (current CPU-time: 14.5208 s) c ============================================================================== c [1mFound solution: 2032[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3970 | 27339 90408 | 8201 2915 121894 41.8 | 22.651 % | c -- subsuming c -- var.elim.: 1000/1043 c -- var.elim.: 1043/1043 c -- var.elim.: 632/632 c -- var.elim.: 174/174 c -- var.elim.: 44/44 c -- var.elim.: 1/1 c -- var.elim.: 18/18 c -- subsuming c -- var.elim.: 44/44 c | 3970 | 26897 89818 | -- 2915 -- -- | -- | -433/-571 c | 3970 | 26897 89818 | 10758 2791 99584 35.7 | 22.651 % | c | 4070 | 26813 89426 | 11797 2889 100588 34.8 | 22.905 % | c | 4220 | 26813 89426 | 12977 3039 114355 37.6 | 22.905 % | c | 4446 | 26803 89373 | 14269 3258 129212 39.7 | 22.967 % | c | 4784 | 26662 88727 | 15614 3582 138753 38.7 | 23.212 % | c ============================================================================== c (current CPU-time: 16.8154 s) c ============================================================================== c [1mFound solution: 2015[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 5144 | 27087 89812 | 8126 3942 189900 48.2 | 23.212 % | c -- subsuming c -- var.elim.: 853/853 c -- var.elim.: 591/591 c -- var.elim.: 310/310 c -- var.elim.: 59/59 c -- subsuming c -- var.elim.: 53/53 c | 5144 | 26623 88397 | -- 3942 -- -- | -- | -454/-1394 c | 5144 | 26623 88397 | 10649 3587 138660 38.7 | 23.212 % | c | 5245 | 26623 88397 | 11714 3688 150829 40.9 | 23.335 % | c | 5396 | 26623 88397 | 12885 3839 160944 41.9 | 23.335 % | c | 5624 | 26613 88365 | 14168 4066 170892 42.0 | 23.347 % | c | 5962 | 26613 88365 | 15585 4404 209697 47.6 | 23.347 % | c | 6470 | 26613 88365 | 17144 4912 256730 52.3 | 23.347 % | c ============================================================================== c (current CPU-time: 20.7248 s) c ============================================================================== c [1mFound solution: 2012[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 6776 | 26595 88332 | 7978 5215 282535 54.2 | 23.347 % | c -- subsuming c -- var.elim.: 184/184 c -- var.elim.: 139/139 c -- var.elim.: 6/6 c | 6776 | 26559 88546 | -- 5215 -- -- | -- | -36/215 c | 6776 | 26559 88546 | 10623 5066 250721 49.5 | 23.347 % | c | 6876 | 26559 88546 | 11685 5166 254397 49.2 | 23.484 % | c | 7026 | 26428 88098 | 12791 5309 257953 48.6 | 23.680 % | c | 7253 | 26340 87766 | 14023 5529 276990 50.1 | 23.852 % | c | 7591 | 26298 87270 | 15401 5864 301955 51.5 | 23.901 % | c | 8097 | 26298 87270 | 16941 6370 386363 60.7 | 23.901 % | c | 8856 | 26165 86673 | 18541 7120 411808 57.8 | 24.133 % | c ============================================================================== c (current CPU-time: 25.2342 s) c ============================================================================== c [1mFound solution: 1847[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 8944 | 26217 86846 | 7865 7208 419748 58.2 | 24.133 % | c -- subsuming c -- var.elim.: 636/636 c -- var.elim.: 392/392 c -- var.elim.: 4/4 c -- subsuming c -- var.elim.: 107/107 c | 8944 | 26113 86794 | -- 7208 -- -- | -- | -104/-51 c | 8944 | 26113 86794 | 10445 6721 304720 45.3 | 24.133 % | c | 9046 | 26005 86435 | 11442 6818 307530 45.1 | 24.428 % | c | 9198 | 26005 86435 | 12586 6970 323614 46.4 | 24.428 % | c | 9423 | 26005 86435 | 13845 7195 333822 46.4 | 24.428 % | c | 9760 | 25980 86357 | 15214 7526 386424 51.3 | 24.465 % | c | 10267 | 25976 86340 | 16733 8032 412658 51.4 | 24.477 % | c | 11026 | 25968 86296 | 18401 8790 515562 58.7 | 24.514 % | c | 12165 | 25893 85795 | 20183 9925 745375 75.1 | 24.600 % | c ============================================================================== c (current CPU-time: 38.3982 s) c ============================================================================== c [1mFound solution: 1814[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 13790 | 25941 85756 | 7782 11545 1110765 96.2 | 24.600 % | c -- subsuming c -- var.elim.: 778/778 c -- var.elim.: 629/629 c -- var.elim.: 126/126 c -- var.elim.: 82/82 c -- subsuming c -- var.elim.: 262/262 c | 13790 | 25803 85662 | -- 11545 -- -- | -- | -138/-93 c | 13790 | 25803 85662 | 10321 10570 821449 77.7 | 24.600 % | c | 13890 | 25780 85581 | 11343 10668 824966 77.3 | 24.845 % | c | 14043 | 25780 85581 | 12477 10821 836349 77.3 | 24.846 % | c | 14272 | 25780 85581 | 13725 11050 895148 81.0 | 24.845 % | c | 14611 | 25780 85581 | 15097 11389 982428 86.3 | 24.846 % | c ============================================================================== c (current CPU-time: 42.3826 s) c ============================================================================== c [1mFound solution: 1780[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 15092 | 25882 85760 | 7764 11841 1071707 90.5 | 24.846 % | c -- subsuming c -- var.elim.: 403/403 c -- var.elim.: 238/238 c -- var.elim.: 87/87 c -- var.elim.: 45/45 c | 15092 | 25766 85707 | -- 11841 -- -- | -- | -116/-52 c | 15092 | 25766 85707 | 10306 9255 373728 40.4 | 24.846 % | c | 15193 | 25766 85707 | 11337 9356 378639 40.5 | 24.929 % | c | 15343 | 25766 85707 | 12470 9506 399748 42.1 | 24.929 % | c | 15571 | 25766 85707 | 13717 9734 427211 43.9 | 24.929 % | c | 15908 | 25766 85707 | 15089 10071 458565 45.5 | 24.929 % | c | 16414 | 25704 85500 | 16558 10572 517872 49.0 | 25.040 % | c | 17173 | 25704 85500 | 18214 11331 613589 54.2 | 25.040 % | c | 18313 | 25432 84539 | 19823 12465 809468 64.9 | 25.437 % | c | 20022 | 25432 84539 | 21806 14174 1159953 81.8 | 25.436 % | c | 22584 | 25355 84262 | 23914 16716 1565392 93.6 | 25.585 % | c ============================================================================== c (current CPU-time: 65.4321 s) c ============================================================================== c [1mFound solution: 1726[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 23653 | 25455 84555 | 7636 17785 1760340 99.0 | 25.585 % | c -- subsuming c -- var.elim.: 632/632 c -- var.elim.: 407/407 c -- var.elim.: 80/80 c -- var.elim.: 30/30 c -- subsuming c -- var.elim.: 51/51 c -- var.elim.: 43/43 c -- var.elim.: 9/9 c | 23653 | 25289 84369 | -- 17785 -- -- | -- | -164/-181 c | 23653 | 25289 84369 | 10115 13159 644206 49.0 | 25.585 % | c | 23753 | 25289 84369 | 11127 8678 494684 57.0 | 25.762 % | c | 23907 | 25289 84369 | 12239 8832 499943 56.6 | 25.762 % | c ============================================================================== c (current CPU-time: 67.2658 s) c ============================================================================== c [1mFound solution: 1449[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 24120 | 25452 84795 | 7635 9045 524739 58.0 | 25.762 % | c -- subsuming c -- var.elim.: 235/235 c -- var.elim.: 150/150 c -- var.elim.: 118/118 c -- var.elim.: 43/43 c | 24120 | 25302 84523 | -- 9045 -- -- | -- | -147/-265 c | 24120 | 25302 84523 | 10120 9045 524739 58.0 | 25.762 % | c | 24223 | 25302 84523 | 11132 9148 533057 58.3 | 25.742 % | c | 24373 | 25291 84450 | 12240 9297 542701 58.4 | 25.754 % | c | 24600 | 25246 84301 | 13440 9523 547503 57.5 | 25.854 % | c | 24937 | 25246 84301 | 14785 9860 602154 61.1 | 25.854 % | c | 25447 | 25246 84301 | 16263 10370 624712 60.2 | 25.854 % | c ============================================================================== c (current CPU-time: 72.484 s) c ============================================================================== c [1mFound solution: 1402[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 26032 | 25301 84390 | 7590 10952 655662 59.9 | 25.854 % | c -- subsuming c -- var.elim.: 409/409 c -- var.elim.: 220/220 c -- var.elim.: 81/81 c -- var.elim.: 1/1 c -- var.elim.: 64/64 c -- subsuming c -- var.elim.: 40/40 c | 26032 | 25176 84175 | -- 10952 -- -- | -- | -124/-212 c | 26032 | 25176 84175 | 10070 10594 585318 55.2 | 25.854 % | c | 26133 | 25176 84175 | 11077 10695 596878 55.8 | 26.051 % | c | 26283 | 25176 84175 | 12185 10845 603087 55.6 | 26.051 % | c | 26508 | 25176 84175 | 13403 11070 612416 55.3 | 26.051 % | c ============================================================================== c (current CPU-time: 74.5357 s) c ============================================================================== c [1mFound solution: 1311[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 26646 | 25236 84347 | 7570 11208 636744 56.8 | 26.051 % | c -- subsuming c -- var.elim.: 94/94 c -- var.elim.: 66/66 c -- var.elim.: 37/37 c -- var.elim.: 27/27 c | 26646 | 25185 84241 | -- 11208 -- -- | -- | -51/-105 c | 26646 | 25185 84241 | 10074 11208 636744 56.8 | 26.051 % | c | 26746 | 25185 84241 | 11081 11308 643920 56.9 | 26.070 % | c | 26897 | 25185 84241 | 12189 11459 663488 57.9 | 26.070 % | c | 27122 | 25177 84213 | 13404 11683 687397 58.8 | 26.095 % | c | 27459 | 24918 82851 | 14592 12012 714949 59.5 | 26.455 % | c | 27965 | 24918 82851 | 16052 12518 812129 64.9 | 26.455 % | c | 28725 | 24918 82851 | 17657 13278 885835 66.7 | 26.455 % | c | 29864 | 24908 82820 | 19415 14394 1089500 75.7 | 26.468 % | c | 31572 | 24908 82820 | 21357 16102 1324979 82.3 | 26.468 % | c ============================================================================== c (current CPU-time: 96.6523 s) c ============================================================================== c [1mFound solution: 1310[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 33381 | 24943 82856 | 7482 17908 1624059 90.7 | 26.468 % | c -- subsuming c -- var.elim.: 651/651 c -- var.elim.: 502/502 c -- var.elim.: 42/42 c -- subsuming c -- var.elim.: 148/148 c -- var.elim.: 12/12 c | 33381 | 24784 82970 | -- 17908 -- -- | -- | -155/123 c | 33381 | 24784 82970 | 9913 15937 1103416 69.2 | 26.468 % | c | 33483 | 24784 82970 | 10904 10727 738250 68.8 | 26.747 % | c | 33634 | 24784 82970 | 11995 10878 769140 70.7 | 26.747 % | c | 33859 | 24784 82970 | 13195 11103 800518 72.1 | 26.747 % | c | 34197 | 24784 82970 | 14514 11441 859118 75.1 | 26.747 % | c | 34704 | 24784 82970 | 15965 11948 916662 76.7 | 26.747 % | c | 35463 | 24784 82970 | 17562 12707 1016593 80.0 | 26.747 % | c | 36602 | 24784 82970 | 19318 13846 1215598 87.8 | 26.747 % | c | 38311 | 24784 82970 | 21250 15555 1628206 104.7 | 26.747 % | c ============================================================================== c (current CPU-time: 122.645 s) c ============================================================================== c [1mFound solution: 1309[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 40778 | 24872 83234 | 7461 18022 2316283 128.5 | 26.747 % | c -- subsuming c -- var.elim.: 162/162 c -- var.elim.: 110/110 c -- var.elim.: 23/23 c -- var.elim.: 57/57 c | 40778 | 24799 83227 | -- 18022 -- -- | -- | -73/-6 c | 40778 | 24799 83227 | 9919 18022 2316283 128.5 | 26.747 % | c | 40878 | 24799 83227 | 10911 12115 1815391 149.8 | 26.752 % | c | 41028 | 24799 83227 | 12002 12265 1838060 149.9 | 26.753 % | c | 41253 | 24799 83227 | 13202 12490 1869026 149.6 | 26.753 % | c | 41590 | 24799 83227 | 14523 12827 1933266 150.7 | 26.753 % | c | 42097 | 24521 82236 | 15796 13243 1949507 147.2 | 27.216 % | c | 42856 | 24521 82236 | 17376 14002 2070473 147.9 | 27.216 % | c | 43997 | 24521 82236 | 19113 15143 2350636 155.2 | 27.215 % | c | 45705 | 24521 82236 | 21025 16851 2716662 161.2 | 27.215 % | c ============================================================================== c (current CPU-time: 140.597 s) c ============================================================================== c [1mFound solution: 1308[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 45915 | 24586 82455 | 7375 17061 2771325 162.4 | 27.215 % | c -- subsuming c -- var.elim.: 372/372 c -- var.elim.: 268/268 c -- var.elim.: 56/56 c -- subsuming c -- var.elim.: 23/23 c | 45915 | 24430 82303 | -- 17061 -- -- | -- | -155/-149 c | 45915 | 24430 82303 | 9772 14303 1553901 108.6 | 27.215 % | c | 46016 | 24430 82303 | 10749 9637 925615 96.0 | 27.428 % | c | 46168 | 24430 82303 | 11824 9789 951268 97.2 | 27.428 % | c | 46393 | 24430 82303 | 13006 10014 1006520 100.5 | 27.428 % | c | 46734 | 24430 82303 | 14307 10355 1100774 106.3 | 27.428 % | c | 47240 | 24430 82303 | 15737 10861 1253178 115.4 | 27.428 % | c | 47999 | 24430 82303 | 17311 11620 1399746 120.5 | 27.428 % | c | 49142 | 24430 82303 | 19042 12763 1640592 128.5 | 27.428 % | c | 50850 | 24430 82303 | 20947 14471 2037581 140.8 | 27.428 % | c ============================================================================== c (current CPU-time: 160.178 s) c ============================================================================== c [1mFound solution: 1239[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 51345 | 24586 82714 | 7375 14966 2144044 143.3 | 27.428 % | c -- subsuming c -- var.elim.: 230/230 c -- var.elim.: 142/142 c -- var.elim.: 95/95 c | 51345 | 24451 82527 | -- 14966 -- -- | -- | -134/-184 c | 51345 | 24451 82527 | 9780 14966 2144044 143.3 | 27.428 % | c | 51445 | 24451 82527 | 10758 10078 1416862 140.6 | 27.418 % | c | 51597 | 24451 82527 | 11834 10230 1419335 138.7 | 27.418 % | c | 51822 | 24451 82527 | 13017 10455 1434677 137.2 | 27.418 % | c | 52161 | 24451 82527 | 14319 10794 1496444 138.6 | 27.418 % | c | 52667 | 24451 82527 | 15751 11300 1583161 140.1 | 27.419 % | c | 53427 | 24451 82527 | 17326 12060 1724362 143.0 | 27.418 % | c ============================================================================== c (current CPU-time: 169.035 s) c ============================================================================== c [1mFound solution: 1236[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 54188 | 24532 82792 | 7359 12821 1838880 143.4 | 27.418 % | c -- subsuming c -- var.elim.: 182/182 c -- var.elim.: 122/122 c -- var.elim.: 58/58 c | 54188 | 24468 82979 | -- 12821 -- -- | -- | -64/188 c | 54188 | 24468 82979 | 9787 12821 1838880 143.4 | 27.418 % | c | 54288 | 24468 82979 | 10765 8648 992458 114.8 | 27.424 % | c | 54439 | 24416 82795 | 11817 8798 1019900 115.9 | 27.499 % | c | 54664 | 24416 82795 | 12999 9023 1043417 115.6 | 27.499 % | c | 55003 | 24416 82795 | 14298 9362 1098525 117.3 | 27.499 % | c | 55509 | 24416 82795 | 15728 9868 1218186 123.4 | 27.499 % | c | 56269 | 24416 82795 | 17301 10628 1419997 133.6 | 27.499 % | c ============================================================================== c (current CPU-time: 181.067 s) c ============================================================================== c [1mFound solution: 1224[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 57406 | 24450 82932 | 7334 11765 1583948 134.6 | 27.499 % | c -- subsuming c -- var.elim.: 150/150 c -- var.elim.: 136/136 c | 57406 | 24423 83068 | -- 11765 -- -- | -- | -27/137 c | 57406 | 24423 83068 | 9769 11439 1454215 127.1 | 27.499 % | c | 57508 | 24423 83068 | 10746 11541 1473748 127.7 | 27.525 % | c | 57660 | 24423 83068 | 11820 11693 1503693 128.6 | 27.525 % | c | 57887 | 24423 83068 | 13002 11920 1561979 131.0 | 27.525 % | c | 58224 | 24423 83068 | 14303 12257 1645527 134.3 | 27.525 % | c | 58731 | 24409 82997 | 15724 12762 1756411 137.6 | 27.550 % | c | 59492 | 24409 82997 | 17296 13523 1908792 141.2 | 27.550 % | c | 60633 | 24409 82997 | 19026 14664 2148519 146.5 | 27.550 % | c | 62341 | 24409 82997 | 20929 16372 2475459 151.2 | 27.550 % | c | 64905 | 24401 82971 | 23014 18934 3033810 160.2 | 27.563 % | c | 68749 | 24401 82971 | 25315 22778 3817870 167.6 | 27.563 % | c | 74516 | 24389 82933 | 27833 16604 2432237 146.5 | 27.588 % | c ============================================================================== c (current CPU-time: 269.514 s) c ============================================================================== c [1mFound solution: 1215[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 78439 | 24467 83151 | 7340 20527 3456586 168.4 | 27.588 % | c -- subsuming c -- var.elim.: 161/161 c -- var.elim.: 211/211 c -- var.elim.: 56/56 c -- var.elim.: 3/3 c -- var.elim.: 1/1 c -- var.elim.: 28/28 c | 78439 | 24400 83086 | -- 20527 -- -- | -- | -65/-60 c | 78439 | 24400 83086 | 9760 18652 3061027 164.1 | 27.588 % | c | 78540 | 24400 83086 | 10736 8391 1199308 142.9 | 27.629 % | c | 78690 | 24372 82983 | 11796 8540 1212130 141.9 | 27.667 % | c | 78915 | 24365 82960 | 12971 8764 1242638 141.8 | 27.679 % | c | 79254 | 24365 82960 | 14269 9103 1292527 142.0 | 27.679 % | c | 79760 | 24365 82960 | 15696 9609 1398154 145.5 | 27.679 % | c | 80519 | 24365 82960 | 17265 10368 1568640 151.3 | 27.679 % | c | 81660 | 24317 82731 | 18954 11508 1697519 147.5 | 27.817 % | c | 83370 | 24317 82731 | 20850 13218 2028793 153.5 | 27.817 % | c | 85932 | 24317 82731 | 22935 15780 2332574 147.8 | 27.817 % | c | 89778 | 24317 82731 | 25228 19626 3180839 162.1 | 27.817 % | c | 95544 | 24302 82666 | 27734 25390 4603343 181.3 | 27.829 % | c | 104193 | 24252 82519 | 30445 20981 3573255 170.3 | 27.942 % | c ============================================================================== c (current CPU-time: 377.692 s) c ============================================================================== c [1mFound solution: 1214[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 104297 | 24385 82884 | 7315 21085 3589623 170.2 | 27.942 % | c -- subsuming c -- var.elim.: 501/501 c -- var.elim.: 208/208 c -- var.elim.: 76/76 c -- var.elim.: 61/61 c -- subsuming c -- var.elim.: 16/16 c | 104297 | 24259 82730 | -- 21085 -- -- | -- | -126/-153 c | 104297 | 24259 82730 | 9703 15388 1503384 97.7 | 27.942 % | c | 104397 | 24259 82730 | 10673 10359 828131 79.9 | 27.993 % | c | 104548 | 24259 82730 | 11741 10510 855769 81.4 | 27.993 % | c | 104773 | 24259 82730 | 12915 10735 893005 83.2 | 27.993 % | c | 105110 | 24259 82730 | 14207 11072 951530 85.9 | 27.993 % | c | 105616 | 24259 82730 | 15627 11578 1035150 89.4 | 27.993 % | c | 106375 | 24259 82730 | 17190 12337 1172004 95.0 | 27.993 % | c | 107514 | 24259 82730 | 18909 13476 1381269 102.5 | 27.993 % | c | 109222 | 24259 82730 | 20800 15184 1722262 113.4 | 27.993 % | c | 111784 | 24259 82730 | 22880 17746 2209358 124.5 | 27.993 % | c ============================================================================== c (current CPU-time: 408.927 s) c ============================================================================== c [1mFound solution: 1195[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 112529 | 24462 83267 | 7338 18491 2386405 129.1 | 27.993 % | c -- subsuming c -- var.elim.: 280/280 c -- var.elim.: 195/195 c -- var.elim.: 114/114 c -- var.elim.: 86/86 c | 112529 | 24270 82947 | -- 18491 -- -- | -- | -189/-313 c | 112529 | 24270 82947 | 9708 18491 2386405 129.1 | 27.993 % | c | 112630 | 24270 82947 | 10678 8320 965798 116.1 | 28.031 % | c | 112781 | 24270 82947 | 11746 8471 986645 116.5 | 28.031 % | c | 113010 | 24270 82947 | 12921 8700 1024074 117.7 | 28.031 % | c | 113349 | 24270 82947 | 14213 9039 1088643 120.4 | 28.031 % | c | 113855 | 24270 82947 | 15634 9545 1200586 125.8 | 28.031 % | c | 114614 | 24270 82947 | 17198 10304 1358694 131.9 | 28.031 % | c | 115753 | 24270 82947 | 18918 11443 1557946 136.1 | 28.031 % | c | 117462 | 24270 82947 | 20809 13152 1933371 147.0 | 28.031 % | c | 120025 | 24270 82947 | 22890 15715 2537150 161.4 | 28.031 % | c ============================================================================== c (current CPU-time: 448.236 s) c ============================================================================== c [1mFound solution: 1149[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 122986 | 24287 83007 | 7286 18676 3218483 172.3 | 28.031 % | c -- subsuming c -- var.elim.: 114/114 c -- var.elim.: 32/32 c | 122986 | 24277 82874 | -- 18676 -- -- | -- | -10/-132 c | 122986 | 24277 82874 | 9710 18676 3218483 172.3 | 28.031 % | c | 123086 | 24277 82874 | 10681 8408 1178962 140.2 | 28.036 % | c | 123236 | 24266 82840 | 11744 8557 1195938 139.8 | 28.049 % | c | 123461 | 24266 82840 | 12919 8782 1223117 139.3 | 28.049 % | c | 123800 | 24266 82840 | 14211 9121 1295383 142.0 | 28.049 % | c | 124307 | 24266 82840 | 15632 9628 1335065 138.7 | 28.049 % | c | 125067 | 24266 82840 | 17195 10388 1464748 141.0 | 28.049 % | c | 126207 | 24266 82840 | 18915 11528 1723854 149.5 | 28.049 % | c ============================================================================== c (current CPU-time: 466.668 s) c ============================================================================== c [1mFound solution: 1145[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 127876 | 24286 82921 | 7285 13197 2096266 158.8 | 28.049 % | c -- subsuming c -- var.elim.: 69/69 c -- var.elim.: 54/54 c | 127876 | 24277 82922 | -- 13197 -- -- | -- | -9/2 c | 127876 | 24277 82922 | 9710 13197 2096266 158.8 | 28.049 % | c | 127976 | 24277 82922 | 10681 8898 1103778 124.0 | 28.058 % | c | 128129 | 24277 82922 | 11750 9051 1128143 124.6 | 28.058 % | c | 128354 | 24277 82922 | 12925 9276 1157851 124.8 | 28.058 % | c | 128691 | 24277 82922 | 14217 9613 1218237 126.7 | 28.058 % | c | 129199 | 24277 82922 | 15639 10121 1286974 127.2 | 28.058 % | c | 129959 | 24277 82922 | 17203 10881 1377423 126.6 | 28.058 % | c | 131099 | 24277 82922 | 18923 12021 1570083 130.6 | 28.058 % | c | 132808 | 24277 82922 | 20815 13730 1909962 139.1 | 28.058 % | c | 135370 | 24277 82922 | 22897 16292 2427004 149.0 | 28.058 % | c | 139220 | 24238 82776 | 25146 20141 3273175 162.5 | 28.108 % | c | 144987 | 24200 82636 | 27618 25906 4446737 171.6 | 28.183 % | c | 153636 | 24200 82636 | 30379 21040 3745103 178.0 | 28.183 % | c ============================================================================== c (current CPU-time: 605.569 s) c ============================================================================== c [1mFound solution: 1136[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 160677 | 24329 82989 | 7298 28081 5595055 199.2 | 28.183 % | c -- subsuming c -- var.elim.: 300/300 c -- var.elim.: 186/186 c -- var.elim.: 55/55 c -- var.elim.: 68/68 c | 160677 | 24207 82898 | -- 28081 -- -- | -- | -122/-90 c | 160677 | 24207 82898 | 9682 27857 5540805 198.9 | 28.183 % | c | 160778 | 24207 82898 | 10651 11847 1798485 151.8 | 28.199 % | c | 160930 | 24207 82898 | 11716 11999 1818640 151.6 | 28.199 % | c | 161158 | 24207 82898 | 12887 12227 1870486 153.0 | 28.199 % | c | 161497 | 24207 82898 | 14176 12566 1930734 153.6 | 28.199 % | c | 162004 | 24207 82898 | 15594 13073 2075002 158.7 | 28.199 % | c | 162764 | 24207 82898 | 17153 13833 2238919 161.9 | 28.199 % | c | 163906 | 24207 82898 | 18869 14975 2487782 166.1 | 28.199 % | c | 165614 | 24207 82898 | 20755 16683 2829132 169.6 | 28.199 % | c | 168176 | 24207 82898 | 22831 19245 3313633 172.2 | 28.199 % | c | 172020 | 24147 82685 | 25052 23079 4243071 183.8 | 28.287 % | c ============================================================================== c (current CPU-time: 681.318 s) c ============================================================================== c [1mFound solution: 1120[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 177119 | 24262 83005 | 7278 28178 5588887 198.3 | 28.287 % | c -- subsuming c -- var.elim.: 217/217 c -- var.elim.: 183/183 c -- var.elim.: 89/89 c -- var.elim.: 1/1 c -- var.elim.: 69/69 c | 177119 | 24151 83084 | -- 28178 -- -- | -- | -108/86 c | 177119 | 24151 83084 | 9660 24767 4192612 169.3 | 28.287 % | c | 177220 | 24151 83084 | 10626 10791 1450723 134.4 | 28.328 % | c | 177370 | 24151 83084 | 11689 10941 1495980 136.7 | 28.328 % | c | 177597 | 24151 83084 | 12857 11168 1511791 135.4 | 28.328 % | c | 177934 | 24151 83084 | 14143 11505 1545060 134.3 | 28.328 % | c | 178440 | 24151 83084 | 15558 12011 1629091 135.6 | 28.328 % | c | 179199 | 24151 83084 | 17113 12770 1763934 138.1 | 28.328 % | c | 180340 | 24151 83084 | 18825 13911 2000481 143.8 | 28.328 % | c | 182048 | 24151 83084 | 20707 15619 2396916 153.5 | 28.328 % | c | 184611 | 24151 83084 | 22778 18182 3177782 174.8 | 28.328 % | c | 188456 | 24151 83084 | 25056 22027 4289247 194.7 | 28.328 % | c | 194223 | 24151 83084 | 27562 27794 5376483 193.4 | 28.328 % | c | 202875 | 24144 83046 | 30309 16559 2531004 152.8 | 28.340 % | c | 215849 | 22350 73670 | 30863 24852 4569151 183.9 | 31.411 % | c ============================================================================== c [1mOptimal solution: 1120[0m s OPTIMUM FOUND v C101_bit0 C102_bit0 -C103_bit0 -C104_bit0 -C105_bit0 -C108_bit0 -C111_bit0 -C112_bit0 -C113_bit0 C114_bit0 -C115_bit0 -C116_bit0 -C117_bit0 -C118_bit0 -C119_bit0 -C120_bit0 -C121_bit0 -C122_bit0 -C123_bit0 -C124_bit0 -C125_bit0 -C126_bit0 C127_bit0 -C128_bit0 -C129_bit0 -C130_bit0 -C131_bit0 -C132_bit0 -C133_bit0 -C134_bit0 C135_bit0 -C136_bit0 -C137_bit0 -C138_bit0 C139_bit0 -C140_bit0 -C141_bit0 -C142_bit0 C143_bit0 -C144_bit0 -C145_bit0 -C146_bit0 -C147_bit0 -C148_bit0 -C149_bit0 -C150_bit0 C151_bit0 -C152_bit0 C153_bit0 -C154_bit0 -C155_bit0 -C156_bit0 -C157_bit0 -C158_bit0 -C159_bit0 -C160_bit0 -C161_bit0 -C162_bit0 -C163_bit0 C164_bit0 -C165_bit0 C166_bit0 -C167_bit0 -C168_bit0 -C169_bit0 -C170_bit0 -C171_bit0 -C172_bit0 -C173_bit0 -C174_bit0 -C175_bit0 -C176_bit0 -C177_bit0 -C178_bit0 -C179_bit0 -C180_bit0 -C181_bit0 -C182_bit0 -C183_bit0 -C184_bit0 -C185_bit0 C186_bit0 -C187_bit0 -C188_bit0 -C189_bit0 -C106_bit0 C107_bit0 -C109_bit0 -C110_bit0 c _______________________________________________________________________________ c c restarts : 224 c conflicts : 225789 (250 /sec) c decisions : 374144 (415 /sec) c propagations : 168540481 (186733 /sec) c inspects : 1209315592 (1339848 /sec) c CPU time : 902.577 s c _______________________________________________________________________________ #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.79 0.92 0.90 2/55 10847 Raw data (stat): 10847 (runsolver) R 10846 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548987898 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0008 s] Raw data (loadavg): 0.82 0.93 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 6099 0 0 0 967 21 0 0 25 0 1 0 548987898 14782464 2879 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3609 2879 603 41 0 3568 0 vsize: 14436 [startup+20.0025 s] Raw data (loadavg): 0.85 0.93 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 8911 0 0 0 1957 31 0 0 25 0 1 0 548987898 14827520 2915 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3620 2915 603 41 0 3579 0 vsize: 14480 [startup+30.0036 s] Raw data (loadavg): 0.87 0.93 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 10338 0 0 0 2952 36 0 0 25 0 1 0 548987898 18178048 3653 4294967295 134512640 134672761 3221224544 3221223680 134614816 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4438 3653 603 41 0 4397 0 vsize: 17752 [startup+40.0035 s] Raw data (loadavg): 0.89 0.93 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 11405 0 0 0 3949 39 0 0 25 0 1 0 548987898 19599360 4081 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4785 4081 603 41 0 4744 0 vsize: 19140 [startup+50.0038 s] Raw data (loadavg): 0.90 0.93 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 12021 0 0 0 4946 42 0 0 25 0 1 0 548987898 21094400 4361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5150 4361 603 41 0 5109 0 vsize: 20600 [startup+60.0042 s] Raw data (loadavg): 0.92 0.93 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 12041 0 0 0 5946 42 0 0 25 0 1 0 548987898 21094400 4381 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5150 4381 603 41 0 5109 0 vsize: 20600 [startup+70.0042 s] Raw data (loadavg): 0.93 0.94 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 13752 0 0 0 6940 49 0 0 25 0 1 0 548987898 21987328 4672 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5368 4672 603 41 0 5327 0 vsize: 21472 [startup+80.0054 s] Raw data (loadavg): 0.94 0.94 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 14882 0 0 0 7934 54 0 0 25 0 1 0 548987898 22085632 4699 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5392 4699 603 41 0 5351 0 vsize: 21568 [startup+90.005 s] Raw data (loadavg): 0.95 0.94 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 14882 0 0 0 8934 54 0 0 25 0 1 0 548987898 22085632 4699 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5392 4699 603 41 0 5351 0 vsize: 21568 [startup+100.005 s] Raw data (loadavg): 0.96 0.94 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 15596 0 0 0 9932 57 0 0 25 0 1 0 548987898 23953408 5071 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5848 5071 603 41 0 5807 0 vsize: 23392 [startup+110.006 s] Raw data (loadavg): 0.96 0.94 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 15596 0 0 0 10932 57 0 0 25 0 1 0 548987898 23953408 5071 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5848 5071 603 41 0 5807 0 vsize: 23392 [startup+120.007 s] Raw data (loadavg): 0.97 0.94 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 15606 0 0 0 11932 57 0 0 25 0 1 0 548987898 23953408 5081 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5848 5081 603 41 0 5807 0 vsize: 23392 [startup+130.008 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 16636 0 0 0 12928 60 0 0 25 0 1 0 548987898 26750976 5745 4294967295 134512640 134672761 3221224544 3221223792 134618022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6531 5745 603 41 0 6490 0 vsize: 26124 [startup+140.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 16675 0 0 0 13928 60 0 0 25 0 1 0 548987898 26750976 5784 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6531 5784 603 41 0 6490 0 vsize: 26124 [startup+150.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 17500 0 0 0 14925 64 0 0 25 0 1 0 548987898 28737536 6265 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7016 6265 603 41 0 6975 0 vsize: 28064 [startup+160.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 17500 0 0 0 15925 64 0 0 25 0 1 0 548987898 28737536 6265 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7016 6265 603 41 0 6975 0 vsize: 28064 [startup+170.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 18704 0 0 0 16920 68 0 0 25 0 1 0 548987898 29663232 6354 4294967295 134512640 134672761 3221224544 3221222924 1075325894 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7242 6354 603 41 0 7201 0 vsize: 28968 [startup+180.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 18808 0 0 0 17919 70 0 0 25 0 1 0 548987898 26386432 5757 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6442 5757 603 41 0 6401 0 vsize: 25768 [startup+190.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 19459 0 0 0 18917 72 0 0 25 0 1 0 548987898 26386432 5757 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6442 5757 603 41 0 6401 0 vsize: 25768 [startup+200.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 19459 0 0 0 19917 72 0 0 25 0 1 0 548987898 26386432 5757 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6442 5757 603 41 0 6401 0 vsize: 25768 [startup+210.01 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 19575 0 0 0 20917 72 0 0 25 0 1 0 548987898 26910720 5873 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6570 5873 603 41 0 6529 0 vsize: 26280 [startup+220.01 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 20094 0 0 0 21915 74 0 0 25 0 1 0 548987898 29016064 6392 4294967295 134512640 134672761 3221224544 3221223584 134612878 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7084 6392 603 41 0 7043 0 vsize: 28336 [startup+230.011 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 20636 0 0 0 22914 75 0 0 25 0 1 0 548987898 31252480 6934 4294967295 134512640 134672761 3221224544 3221223680 134614551 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7630 6934 603 41 0 7589 0 vsize: 30520 [startup+240.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 21075 0 0 0 23913 77 0 0 25 0 1 0 548987898 33099776 7373 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8081 7373 603 41 0 8040 0 vsize: 32324 [startup+250.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 21492 0 0 0 24912 78 0 0 25 0 1 0 548987898 34811904 7790 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8499 7790 603 41 0 8458 0 vsize: 33996 [startup+260.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 21722 0 0 0 25911 79 0 0 25 0 1 0 548987898 35721216 8020 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8721 8020 603 41 0 8680 0 vsize: 34884 [startup+270.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10847 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 21723 0 0 0 26911 79 0 0 25 0 1 0 548987898 35721216 8021 4294967295 134512640 134672761 3221224544 3221223584 134603555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8721 8021 603 41 0 8680 0 vsize: 34884 [startup+280.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22410 0 0 0 27908 82 0 0 25 0 1 0 548987898 37330944 8336 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9114 8336 603 41 0 9073 0 vsize: 36456 [startup+290.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22410 0 0 0 28908 82 0 0 25 0 1 0 548987898 37330944 8336 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9114 8336 603 41 0 9073 0 vsize: 36456 [startup+300.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 29908 82 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9114 8337 603 41 0 9073 0 vsize: 36456 [startup+310.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 30908 82 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223584 134612578 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9114 8337 603 41 0 9073 0 vsize: 36456 [startup+320.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 31907 83 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9114 8337 603 41 0 9073 0 vsize: 36456 [startup+330.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 32907 83 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9114 8337 603 41 0 9073 0 vsize: 36456 [startup+340.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 33907 83 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9114 8337 603 41 0 9073 0 vsize: 36456 [startup+350.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22438 0 0 0 34907 83 0 0 25 0 1 0 548987898 37330944 8364 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9114 8364 603 41 0 9073 0 vsize: 36456 [startup+360.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22761 0 0 0 35906 85 0 0 25 0 1 0 548987898 38506496 8687 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9401 8687 603 41 0 9360 0 vsize: 37604 [startup+370.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22952 0 0 0 36905 85 0 0 25 0 1 0 548987898 39231488 8878 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9578 8878 603 41 0 9537 0 vsize: 38312 [startup+380.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 23627 0 0 0 37903 88 0 0 25 0 1 0 548987898 39976960 9059 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9760 9059 603 41 0 9719 0 vsize: 39040 [startup+390.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 23627 0 0 0 38903 88 0 0 25 0 1 0 548987898 39976960 9059 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9760 9059 603 41 0 9719 0 vsize: 39040 [startup+400.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 23627 0 0 0 39903 88 0 0 25 0 1 0 548987898 39976960 9059 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9760 9059 603 41 0 9719 0 vsize: 39040 [startup+410.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24099 0 0 0 40902 90 0 0 25 0 1 0 548987898 42627072 9531 4294967295 134512640 134672761 3221224544 3221222920 1075384033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10407 9531 603 41 0 10366 0 vsize: 41628 [startup+420.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24126 0 0 0 41901 91 0 0 25 0 1 0 548987898 40288256 9143 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9836 9143 603 41 0 9795 0 vsize: 39344 [startup+430.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24126 0 0 0 42901 91 0 0 25 0 1 0 548987898 40288256 9143 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9836 9143 603 41 0 9795 0 vsize: 39344 [startup+440.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24126 0 0 0 43900 91 0 0 25 0 1 0 548987898 40288256 9143 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9836 9143 603 41 0 9795 0 vsize: 39344 [startup+450.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24599 0 0 0 44897 94 0 0 25 0 1 0 548987898 39202816 8878 4294967295 134512640 134672761 3221224544 3221223800 134616156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9571 8878 603 41 0 9530 0 vsize: 38284 [startup+460.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24599 0 0 0 45897 95 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+470.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 46895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+480.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 47895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+490.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 48895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+500.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 49895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+510.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 50895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+520.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 51895 98 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+530.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 52895 98 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+540.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 53895 98 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+550.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 54895 98 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9570 8877 603 41 0 9529 0 vsize: 38280 [startup+560.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 55895 99 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9597 8903 603 41 0 9556 0 vsize: 38388 [startup+570.031 s] Raw data (loadavg): 1.07 0.99 0.91 2/55 10849 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 56894 99 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9597 8903 603 41 0 9556 0 vsize: 38388 [startup+580.033 s] Raw data (loadavg): 1.06 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 57894 100 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9597 8903 603 41 0 9556 0 vsize: 38388 [startup+590.034 s] Raw data (loadavg): 1.05 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 58894 100 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9597 8903 603 41 0 9556 0 vsize: 38388 [startup+600.034 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 59894 100 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9597 8903 603 41 0 9556 0 vsize: 38388 [startup+610.034 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26077 0 0 0 60891 103 0 0 25 0 1 0 548987898 41435136 9345 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10116 9345 603 41 0 10075 0 vsize: 40464 [startup+620.041 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26077 0 0 0 61891 103 0 0 25 0 1 0 548987898 41435136 9345 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10116 9345 603 41 0 10075 0 vsize: 40464 [startup+630.042 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26077 0 0 0 62892 103 0 0 25 0 1 0 548987898 41435136 9345 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10116 9345 603 41 0 10075 0 vsize: 40464 [startup+640.043 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26078 0 0 0 63891 104 0 0 25 0 1 0 548987898 41435136 9346 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10116 9346 603 41 0 10075 0 vsize: 40464 [startup+650.043 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26078 0 0 0 64891 104 0 0 25 0 1 0 548987898 41435136 9346 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10116 9346 603 41 0 10075 0 vsize: 40464 [startup+660.044 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26078 0 0 0 65891 104 0 0 25 0 1 0 548987898 41435136 9346 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10116 9346 603 41 0 10075 0 vsize: 40464 [startup+670.045 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26079 0 0 0 66891 104 0 0 25 0 1 0 548987898 41435136 9347 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10116 9347 603 41 0 10075 0 vsize: 40464 [startup+680.046 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26079 0 0 0 67891 105 0 0 25 0 1 0 548987898 41435136 9347 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10116 9347 603 41 0 10075 0 vsize: 40464 [startup+690.047 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26543 0 0 0 68889 107 0 0 25 0 1 0 548987898 42008576 9498 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9498 603 41 0 10215 0 vsize: 41024 [startup+700.047 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26544 0 0 0 69889 107 0 0 25 0 1 0 548987898 42008576 9499 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9499 603 41 0 10215 0 vsize: 41024 [startup+710.048 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26544 0 0 0 70889 107 0 0 25 0 1 0 548987898 42008576 9499 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9499 603 41 0 10215 0 vsize: 41024 [startup+720.048 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26544 0 0 0 71889 107 0 0 25 0 1 0 548987898 42008576 9499 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9499 603 41 0 10215 0 vsize: 41024 [startup+730.049 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26544 0 0 0 72889 107 0 0 25 0 1 0 548987898 42008576 9499 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9499 603 41 0 10215 0 vsize: 41024 [startup+740.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 73888 108 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223584 134612771 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+750.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 74888 108 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+760.051 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 75888 109 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+770.051 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 76888 109 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223528 1075347105 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+780.053 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 77887 110 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+790.054 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 78887 110 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223680 134614683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+800.054 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 79886 110 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+810.055 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 80886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+820.055 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 81886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+830.056 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 82886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+840.056 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 83886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+850.057 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 84886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9501 603 41 0 10215 0 vsize: 41024 [startup+860.058 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26547 0 0 0 85885 112 0 0 25 0 1 0 548987898 42008576 9502 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9502 603 41 0 10215 0 vsize: 41024 [startup+870.059 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10851 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26547 0 0 0 86885 112 0 0 25 0 1 0 548987898 42008576 9502 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9502 603 41 0 10215 0 vsize: 41024 [startup+880.06 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10853 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26547 0 0 0 87885 113 0 0 25 0 1 0 548987898 42008576 9502 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10256 9502 603 41 0 10215 0 vsize: 41024 [startup+890.061 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10853 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26726 0 0 0 88884 114 0 0 25 0 1 0 548987898 42532864 9681 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10384 9681 603 41 0 10343 0 vsize: 41536 [startup+900.062 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10853 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 27169 0 0 0 89883 115 0 0 25 0 1 0 548987898 44249088 10090 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10803 10090 603 41 0 10762 0 vsize: 43212 [startup+903.835 s] Raw data (loadavg): 1.00 0.99 0.91 1/54 10853 Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 27169 0 0 0 89883 115 0 0 25 0 1 0 548987898 44249088 10090 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10803 10090 603 41 0 10762 0 vsize: 0 Child status: 30 Real time (s): 903.835 CPU time (s): 903.762 CPU user time (s): 902.584 CPU system time (s): 1.17782 CPU usage (%): 99.9919 Max. virtual memory (Kb): 43212 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1120 #### END VERIFIER DATA ####