Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0201.opb |
MD5SUM | ffa3a55eb53181880328dd1b84f91e66 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1523 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 201 |
Biggest coefficient in the objective function | 1920 |
Number of bits for the biggest coefficient in the objective function | 11 |
Sum of the numbers in the objective function | 19980 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 1920 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 19980 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02184 |
Number of variables | 201 |
Total number of constraints | 334 |
Number of constraints which are clauses | 20 |
Number of constraints which are cardinality constraints (but not clauses) | 227 |
Number of constraints which are nor clauses,nor cardinality constraints | 87 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 67 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc18 THE 2005-04-21 17:43:14 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17119 boxname=wulflinc18 idbench=1317 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ffa3a55eb53181880328dd1b84f91e66 /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-p0201.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-p0201.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-p0201.opb IDLAUNCH: 17119 /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: 826664 kB Buffers: 8228 kB Cached: 177124 kB SwapCached: 764 kB Active: 61688 kB Inactive: 125676 kB HighTotal: 131008 kB HighFree: 336 kB LowTotal: 903652 kB LowFree: 826328 kB SwapTotal: 2097892 kB SwapFree: 2096152 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5100 kB Slab: 14976 kB Committed_AS: 63816 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 18:03:17 (client local time) WITH STATUS 10 IN 1200.13 SECONDS stats: 17119 7 1200.13 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 133 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): sssss c ---[ 137]---> BDD-cost: 3 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 15 c ---[ 131]---> BDD-cost: 15 c ---[ 129]---> BDD-cost: 15 c ---[ 127]---> BDD-cost: 15 c ---[ 125]---> BDD-cost: 15 c ---[ 123]---> BDD-cost: 15 c ---[ 121]---> BDD-cost: 15 c ---[ 119]---> BDD-cost: 15 c ---[ 117]---> BDD-cost: 15 c ---[ 115]---> BDD-cost: 15 c ---[ 113]---> BDD-cost: 15 c ---[ 111]---> BDD-cost: 15 c ---[ 109]---> BDD-cost: 15 c ---[ 107]---> BDD-cost: 15 c ---[ 105]---> BDD-cost: 15 c ---[ 103]---> BDD-cost: 15 c ---[ 101]---> BDD-cost: 15 c ---[ 99]---> BDD-cost: 15 c ---[ 97]---> BDD-cost: 15 c ---[ 95]---> BDD-cost: 15 c ---[ 89]---> BDD-cost: 39 c ---[ 88]---> BDD-cost: 42 c ---[ 87]---> BDD-cost: 42 c ---[ 86]---> BDD-cost: 54 c ---[ 85]---> BDD-cost: 73 c ---[ 84]---> BDD-cost: 73 c ---[ 83]---> BDD-cost: 98 c ---[ 82]---> BDD-cost: 85 c ---[ 81]---> BDD-cost: 85 c ---[ 80]---> BDD-cost: 160 c ---[ 79]---> BDD-cost: 107 c ---[ 78]---> BDD-cost: 107 c ---[ 77]---> BDD-cost: 201 c ---[ 76]---> BDD-cost: 128 c ---[ 75]---> BDD-cost: 128 c ---[ 74]---> BDD-cost: 241 c ---[ 73]---> BDD-cost: 150 c ---[ 72]---> BDD-cost: 150 c ---[ 71]---> BDD-cost: 281 c ---[ 70]---> BDD-cost: 172 c ---[ 69]---> BDD-cost: 172 c ---[ 68]---> BDD-cost: 321 c ---[ 67]---> BDD-cost: 194 c ---[ 66]---> BDD-cost: 194 c ---[ 65]---> BDD-cost: 361 c ---[ 64]---> BDD-cost: 3 c ---[ 63]---> BDD-cost: 3 c ---[ 62]---> BDD-cost: 3 c ---[ 61]---> BDD-cost: 3 c ---[ 60]---> BDD-cost: 3 c ---[ 59]---> BDD-cost: 3 c ---[ 58]---> BDD-cost: 9 c ---[ 57]---> BDD-cost: 11 c ---[ 56]---> BDD-cost: 11 c ---[ 55]---> BDD-cost: 9 c ---[ 54]---> BDD-cost: 11 c ---[ 53]---> BDD-cost: 11 c ---[ 52]---> BDD-cost: 9 c ---[ 51]---> BDD-cost: 11 c ---[ 50]---> BDD-cost: 11 c ---[ 49]---> BDD-cost: 9 c ---[ 48]---> BDD-cost: 11 c ---[ 47]---> BDD-cost: 11 c ---[ 46]---> BDD-cost: 9 c ---[ 45]---> BDD-cost: 11 c ---[ 44]---> BDD-cost: 11 c ---[ 43]---> BDD-cost: 9 c ---[ 42]---> BDD-cost: 11 c ---[ 41]---> BDD-cost: 11 c ---[ 40]---> BDD-cost: 9 c ---[ 39]---> BDD-cost: 11 c ---[ 38]---> BDD-cost: 11 c ---[ 37]---> BDD-cost: 9 c ---[ 36]---> BDD-cost: 11 c ---[ 35]---> BDD-cost: 11 c ---[ 34]---> BDD-cost: 9 c ---[ 33]---> BDD-cost: 11 c ---[ 32]---> BDD-cost: 11 c ---[ 31]---> BDD-cost: 9 c ---[ 30]---> BDD-cost: 11 c ---[ 29]---> BDD-cost: 11 c ---[ 28]---> BDD-cost: 9 c ---[ 27]---> BDD-cost: 11 c ---[ 26]---> BDD-cost: 11 c ---[ 25]---> BDD-cost: 9 c ---[ 24]---> BDD-cost: 11 c ---[ 23]---> BDD-cost: 11 c ---[ 22]---> BDD-cost: 9 c ---[ 21]---> BDD-cost: 11 c ---[ 20]---> BDD-cost: 11 c ---[ 19]---> BDD-cost: 9 c ---[ 18]---> BDD-cost: 11 c ---[ 17]---> BDD-cost: 11 c ---[ 16]---> BDD-cost: 9 c ---[ 15]---> BDD-cost: 11 c ---[ 14]---> BDD-cost: 11 c ---[ 13]---> BDD-cost: 9 c ---[ 12]---> BDD-cost: 11 c ---[ 11]---> BDD-cost: 11 c ---[ 10]---> BDD-cost: 9 c ---[ 9]---> BDD-cost: 11 c ---[ 8]---> BDD-cost: 11 c ---[ 7]---> BDD-cost: 9 c ---[ 6]---> BDD-cost: 11 c ---[ 5]---> BDD-cost: 11 c ---[ 4]---> BDD-cost: 1 c ---[ 3]---> BDD-cost: 1 c ---[ 2]---> BDD-cost: 1 c ---[ 1]---> BDD-cost: 1 c ---[ 0]---> BDD-cost: 1 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 11741 34621 | 3522 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/4624 c -- var.elim.: 2000/4624 c -- var.elim.: 3000/4624 c -- var.elim.: 4000/4624 c -- var.elim.: 4624/4624 c -- var.elim.: 1000/1249 c -- var.elim.: 1249/1249 c -- subsuming c -- var.elim.: 1000/1056 c -- var.elim.: 1056/1056 c -- var.elim.: 355/355 c -- subsuming c -- var.elim.: 60/60 c | 0 | 10127 50233 | -- 0 -- -- | -- | -1614/15927 c | 0 | 10127 50233 | 4050 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 1.2878 s) c ============================================================================== c [1mFound solution: 2179[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:21098 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 29 | 56899 159451 | 17069 29 236 8.1 | 0.000 % | c -- subsuming c -- var.elim.: 1000/18366 c -- var.elim.: 2000/18366 c -- var.elim.: 3000/18366 c -- var.elim.: 4000/18366 c -- var.elim.: 5000/18366 c -- var.elim.: 6000/18366 c -- var.elim.: 7000/18366 c -- var.elim.: 8000/18366 c -- var.elim.: 9000/18366 c -- var.elim.: 10000/18366 c -- var.elim.: 11000/18366 c -- var.elim.: 12000/18366 c -- var.elim.: 13000/18366 c -- var.elim.: 14000/18366 c -- var.elim.: 15000/18366 c -- var.elim.: 16000/18366 c -- var.elim.: 17000/18366 c -- var.elim.: 18000/18366 c -- var.elim.: 18366/18366 c -- var.elim.: 1000/9788 c -- var.elim.: 2000/9788 c -- var.elim.: 3000/9788 c -- var.elim.: 4000/9788 c -- var.elim.: 5000/9788 c -- var.elim.: 6000/9788 c -- var.elim.: 7000/9788 c -- var.elim.: 8000/9788 c -- var.elim.: 9000/9788 c -- var.elim.: 9788/9788 c -- var.elim.: 226/226 c -- var.elim.: 379/379 c -- subsuming c -- var.elim.: 1000/2416 c -- var.elim.: 2000/2416 c -- var.elim.: 2416/2416 c -- var.elim.: 810/810 c -- var.elim.: 85/85 c -- subsuming c -- var.elim.: 286/286 c -- var.elim.: 32/32 c | 29 | 50913 185351 | -- 29 -- -- | -- | -5986/25901 c | 29 | 50913 185351 | 20365 29 236 8.1 | 0.000 % | c | 129 | 50534 183439 | 22234 126 2017 16.0 | 1.251 % | c | 280 | 46387 169012 | 22451 236 5240 22.2 | 6.332 % | c | 505 | 45858 167232 | 24414 452 43000 95.1 | 7.017 % | c | 842 | 45791 167030 | 26817 782 68357 87.4 | 7.175 % | c ============================================================================== c (current CPU-time: 8.16476 s) c ============================================================================== c [1mFound solution: 2110[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 988 | 46055 167801 | 13816 927 81633 88.1 | 7.175 % | c -- subsuming c -- var.elim.: 1000/2384 c -- var.elim.: 2000/2384 c -- var.elim.: 2384/2384 c -- var.elim.: 1000/2123 c -- var.elim.: 2000/2123 c -- var.elim.: 2123/2123 c -- var.elim.: 940/940 c -- var.elim.: 786/786 c -- var.elim.: 387/387 c -- subsuming c -- var.elim.: 928/928 c -- var.elim.: 98/98 c | 988 | 44981 166457 | -- 927 -- -- | -- | -1069/-1333 c | 988 | 44981 166457 | 17992 720 32289 44.8 | 7.175 % | c | 1088 | 44981 166457 | 19791 820 38955 47.5 | 7.806 % | c | 1239 | 44889 166018 | 21726 969 44833 46.3 | 7.899 % | c ============================================================================== c (current CPU-time: 10.2414 s) c ============================================================================== c [1mFound solution: 2058[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1441 | 44975 165863 | 13492 1168 57904 49.6 | 7.899 % | c -- subsuming c -- var.elim.: 1000/1580 c -- var.elim.: 1580/1580 c -- var.elim.: 791/791 c -- var.elim.: 328/328 c -- var.elim.: 326/326 c -- var.elim.: 227/227 c -- subsuming c -- var.elim.: 359/359 c -- var.elim.: 39/39 c | 1441 | 44674 165701 | -- 1168 -- -- | -- | -296/-151 c | 1441 | 44674 165701 | 17869 1154 54983 47.6 | 7.899 % | c | 1541 | 44674 165701 | 19656 1254 77529 61.8 | 8.255 % | c | 1691 | 44513 165154 | 21544 1403 82178 58.6 | 8.426 % | c | 1917 | 44310 163959 | 23590 1628 113721 69.9 | 8.611 % | c | 2254 | 41256 151869 | 24161 1903 128053 67.3 | 12.260 % | c ============================================================================== c (current CPU-time: 13.268 s) c ============================================================================== c [1mFound solution: 2040[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2573 | 40659 149690 | 12197 2210 143432 64.9 | 12.260 % | c -- subsuming c -- var.elim.: 1000/2386 c -- var.elim.: 2000/2386 c -- var.elim.: 2386/2386 c -- var.elim.: 1000/2019 c -- var.elim.: 2000/2019 c -- var.elim.: 2019/2019 c -- var.elim.: 573/573 c -- var.elim.: 753/753 c -- var.elim.: 251/251 c -- var.elim.: 68/68 c -- subsuming c -- var.elim.: 929/929 c -- var.elim.: 141/141 c -- var.elim.: 9/9 c | 2573 | 40038 150349 | -- 2210 -- -- | -- | -619/664 c | 2573 | 40038 150349 | 16015 1853 63009 34.0 | 12.260 % | c | 2673 | 40024 150300 | 17610 1952 64440 33.0 | 13.505 % | c | 2825 | 40024 150300 | 19371 2103 74331 35.3 | 13.505 % | c | 3050 | 39895 149523 | 21240 2322 88414 38.1 | 13.648 % | c ============================================================================== c (current CPU-time: 15.4367 s) c ============================================================================== c [1mFound solution: 2018[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3129 | 39929 149755 | 11978 2401 96552 40.2 | 13.648 % | c -- subsuming c -- var.elim.: 548/548 c -- var.elim.: 413/413 c -- var.elim.: 103/103 c -- subsuming c -- var.elim.: 169/169 c | 3129 | 39879 150331 | -- 2401 -- -- | -- | -49/579 c | 3129 | 39879 150331 | 15951 2354 92182 39.2 | 13.648 % | c | 3229 | 39879 150331 | 17546 2454 94173 38.4 | 13.681 % | c | 3379 | 38941 146564 | 18847 2578 100269 38.9 | 14.685 % | c | 3604 | 38570 145283 | 20534 2792 102951 36.9 | 15.163 % | c | 3942 | 38489 145013 | 22540 3124 140677 45.0 | 15.267 % | c ============================================================================== c (current CPU-time: 18.2262 s) c ============================================================================== c [1mFound solution: 1993[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 4440 | 38344 144720 | 11503 3614 190783 52.8 | 15.267 % | c -- subsuming c -- var.elim.: 1000/1125 c -- var.elim.: 1125/1125 c -- var.elim.: 1000/1068 c -- var.elim.: 1068/1068 c -- var.elim.: 423/423 c -- var.elim.: 241/241 c -- var.elim.: 80/80 c -- subsuming c -- var.elim.: 196/196 c -- var.elim.: 33/33 c | 4440 | 37876 143859 | -- 3614 -- -- | -- | -467/-858 c | 4440 | 37876 143859 | 15150 3176 118170 37.2 | 15.267 % | c | 4540 | 37876 143859 | 16665 3276 122353 37.3 | 15.956 % | c | 4691 | 37876 143859 | 18331 3427 128267 37.4 | 15.956 % | c | 4917 | 37603 142710 | 20019 3649 141340 38.7 | 16.206 % | c | 5254 | 37430 142133 | 21920 3977 148730 37.4 | 16.400 % | c ============================================================================== c (current CPU-time: 21.0888 s) c ============================================================================== c [1mFound solution: 1919[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 5517 | 37608 142689 | 11282 4236 213097 50.3 | 16.400 % | c -- subsuming c -- var.elim.: 887/887 c -- var.elim.: 816/816 c -- var.elim.: 32/32 c -- var.elim.: 2/2 c -- subsuming c -- var.elim.: 209/209 c -- var.elim.: 8/8 c | 5517 | 37391 143162 | -- 4236 -- -- | -- | -201/509 c | 5517 | 37391 143162 | 14956 4081 156873 38.4 | 16.400 % | c | 5618 | 37178 142079 | 16358 4180 160211 38.3 | 16.815 % | c | 5768 | 37072 141708 | 17942 4323 163200 37.8 | 16.944 % | c | 5993 | 37066 141689 | 19733 4547 182718 40.2 | 16.960 % | c | 6330 | 37066 141689 | 21707 4884 201052 41.2 | 16.960 % | c | 6836 | 37066 141689 | 23878 5390 255312 47.4 | 16.960 % | c ============================================================================== c (current CPU-time: 24.9662 s) c ============================================================================== c [1mFound solution: 1858[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 6936 | 37156 142034 | 11146 5490 258105 47.0 | 16.960 % | c -- subsuming c -- var.elim.: 652/652 c -- var.elim.: 620/620 c -- var.elim.: 158/158 c -- subsuming c -- var.elim.: 226/226 c -- var.elim.: 4/4 c | 6936 | 37042 142973 | -- 5490 -- -- | -- | -107/955 c | 6936 | 37042 142973 | 14816 5034 192376 38.2 | 16.960 % | c | 7037 | 37042 142973 | 16298 5135 196980 38.4 | 17.038 % | c | 7187 | 37037 142953 | 17925 5280 213049 40.4 | 17.046 % | c | 7412 | 36740 140951 | 19560 5502 223844 40.7 | 17.346 % | c | 7749 | 36740 140951 | 21516 5839 246654 42.2 | 17.346 % | c | 8257 | 36288 139349 | 23376 6321 275380 43.6 | 17.775 % | c ============================================================================== c (current CPU-time: 29.7365 s) c ============================================================================== c [1mFound solution: 1796[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 8603 | 36384 139721 | 10915 6667 301298 45.2 | 17.775 % | c -- subsuming c -- var.elim.: 949/949 c -- var.elim.: 762/762 c -- var.elim.: 165/165 c -- var.elim.: 67/67 c -- subsuming c -- var.elim.: 169/169 c -- var.elim.: 21/21 c | 8603 | 36194 139857 | -- 6667 -- -- | -- | -184/149 c | 8603 | 36194 139857 | 14477 6398 269179 42.1 | 17.775 % | c | 8704 | 36194 139857 | 15925 6499 275431 42.4 | 17.961 % | c | 8859 | 36194 139857 | 17517 6654 288899 43.4 | 17.961 % | c | 9085 | 36194 139857 | 19269 6880 306911 44.6 | 17.961 % | c ============================================================================== c (current CPU-time: 31.9431 s) c ============================================================================== c [1mFound solution: 1728[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 9294 | 36288 140259 | 10886 7089 333913 47.1 | 17.961 % | c -- subsuming c -- var.elim.: 308/308 c -- var.elim.: 303/303 c -- var.elim.: 176/176 c -- var.elim.: 178/178 c | 9294 | 36196 140155 | -- 7089 -- -- | -- | -90/-99 c | 9294 | 36196 140155 | 14478 7009 322443 46.0 | 17.961 % | c | 9394 | 36196 140155 | 15926 7109 327399 46.1 | 17.972 % | c | 9546 | 36123 139915 | 17483 7257 343350 47.3 | 18.054 % | c | 9771 | 36123 139915 | 19231 7482 368335 49.2 | 18.054 % | c | 10109 | 35606 137861 | 20852 7808 393186 50.4 | 18.616 % | c | 10615 | 35606 137861 | 22937 8314 459656 55.3 | 18.616 % | c | 11376 | 35606 137861 | 25231 9075 586055 64.6 | 18.616 % | c | 12515 | 35585 137796 | 27738 10211 752344 73.7 | 18.665 % | c | 14225 | 34605 133995 | 29671 11893 1023732 86.1 | 19.886 % | c | 16788 | 34605 133995 | 32638 14456 1234156 85.4 | 19.886 % | c ============================================================================== c (current CPU-time: 53.7028 s) c ============================================================================== c [1mFound solution: 1721[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 17072 | 34625 134143 | 10387 14740 1286555 87.3 | 19.886 % | c -- subsuming c -- var.elim.: 1000/1306 c -- var.elim.: 1306/1306 c -- var.elim.: 1000/1321 c -- var.elim.: 1321/1321 c -- var.elim.: 683/683 c -- var.elim.: 618/618 c -- var.elim.: 187/187 c -- subsuming c -- var.elim.: 848/848 c -- var.elim.: 452/452 c | 17072 | 34341 135086 | -- 14740 -- -- | -- | -283/946 c | 17072 | 34341 135086 | 13736 11943 611032 51.2 | 19.886 % | c | 17172 | 34341 135086 | 15110 12043 625869 52.0 | 20.210 % | c | 17322 | 34130 134362 | 16518 12188 631029 51.8 | 20.458 % | c | 17547 | 34130 134362 | 18170 12413 645645 52.0 | 20.458 % | c | 17884 | 34130 134362 | 19987 12750 688033 54.0 | 20.458 % | c | 18392 | 34109 134297 | 21973 13255 790711 59.7 | 20.508 % | c | 19151 | 34061 134056 | 24136 14011 867175 61.9 | 20.615 % | c | 20292 | 34029 133955 | 26525 15144 972095 64.2 | 20.681 % | c | 22000 | 34024 133939 | 29173 16851 1279425 75.9 | 20.690 % | c | 24563 | 34024 133939 | 32090 19414 1805068 93.0 | 20.690 % | c | 28408 | 34024 133939 | 35299 23259 2575438 110.7 | 20.690 % | c | 34174 | 33527 130779 | 38262 28982 3507655 121.0 | 21.227 % | c ============================================================================== c (current CPU-time: 111.881 s) c ============================================================================== c [1mFound solution: 1714[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 35166 | 33615 131092 | 10084 29971 3629557 121.1 | 21.227 % | c -- subsuming c -- var.elim.: 1000/1757 c -- var.elim.: 1757/1757 c -- var.elim.: 1000/1324 c -- var.elim.: 1324/1324 c -- var.elim.: 43/43 c -- var.elim.: 78/78 c -- subsuming c -- var.elim.: 722/722 c -- var.elim.: 204/204 c | 35166 | 33410 131988 | -- 29971 -- -- | -- | -203/901 c | 35166 | 33410 131988 | 13364 22099 1078456 48.8 | 21.227 % | c | 35266 | 33410 131988 | 14700 10537 379123 36.0 | 21.413 % | c | 35416 | 33197 130747 | 16067 10685 385857 36.1 | 21.630 % | c | 35642 | 33197 130747 | 17674 10911 412111 37.8 | 21.630 % | c | 35981 | 33161 130634 | 19420 11241 443750 39.5 | 21.713 % | c | 36487 | 33161 130634 | 21362 11747 532184 45.3 | 21.713 % | c | 37246 | 33161 130634 | 23498 12506 659820 52.8 | 21.713 % | c | 38386 | 33161 130634 | 25848 13646 866368 63.5 | 21.713 % | c | 40095 | 33147 130589 | 28421 15354 1198982 78.1 | 21.730 % | c ============================================================================== c (current CPU-time: 126.869 s) c ============================================================================== c [1mFound solution: 1710[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 40229 | 32917 129102 | 9875 15479 1210468 78.2 | 21.730 % | c -- subsuming c -- var.elim.: 987/987 c -- var.elim.: 1000/1067 c -- var.elim.: 1067/1067 c -- var.elim.: 425/425 c -- var.elim.: 288/288 c -- subsuming c -- var.elim.: 532/532 c | 40229 | 32735 130137 | -- 15479 -- -- | -- | -178/1044 c | 40229 | 32735 130137 | 13094 15479 1210468 78.2 | 21.730 % | c | 40329 | 32735 130137 | 14403 15579 1212674 77.8 | 22.201 % | c | 40479 | 32735 130137 | 15843 15729 1215941 77.3 | 22.201 % | c | 40705 | 32735 130137 | 17428 15955 1252593 78.5 | 22.201 % | c | 41042 | 32735 130137 | 19170 16292 1287697 79.0 | 22.201 % | c | 41548 | 32519 129382 | 20948 15841 947215 59.8 | 22.435 % | c | 42307 | 32512 129362 | 23038 16599 1076177 64.8 | 22.444 % | c | 43446 | 32507 129342 | 25338 17725 1282169 72.3 | 22.452 % | c | 45154 | 32507 129342 | 27872 19433 1667376 85.8 | 22.452 % | c | 47716 | 32280 128496 | 30445 21978 2143494 97.5 | 22.703 % | c | 51560 | 32231 128349 | 33439 25815 3047085 118.0 | 22.762 % | c ============================================================================== c (current CPU-time: 184.094 s) c ============================================================================== c [1mFound solution: 1707[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 56576 | 32447 128955 | 9734 30828 4095135 132.8 | 22.762 % | c -- subsuming c -- var.elim.: 860/860 c -- var.elim.: 586/586 c -- var.elim.: 49/49 c -- subsuming c -- var.elim.: 151/151 c | 56576 | 32227 128890 | -- 30828 -- -- | -- | -210/-44 c | 56576 | 32227 128890 | 12890 25126 1914313 76.2 | 22.762 % | c | 56677 | 32227 128890 | 14179 13017 967020 74.3 | 22.872 % | c | 56827 | 32227 128890 | 15597 13167 987913 75.0 | 22.872 % | c | 57052 | 32222 128874 | 17154 13390 1004408 75.0 | 22.880 % | c | 57390 | 32222 128874 | 18870 13728 1045288 76.1 | 22.880 % | c | 57897 | 32191 128762 | 20737 14234 1129254 79.3 | 22.914 % | c ============================================================================== c (current CPU-time: 191.914 s) c ============================================================================== c [1mFound solution: 1706[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 58590 | 32210 128907 | 9662 14927 1226559 82.2 | 22.914 % | c -- subsuming c -- var.elim.: 160/160 c -- var.elim.: 199/199 c -- var.elim.: 49/49 c | 58590 | 32194 128893 | -- 14927 -- -- | -- | -16/-13 c | 58590 | 32194 128893 | 12877 13669 884745 64.7 | 22.914 % | c | 58691 | 32194 128893 | 14165 13770 902436 65.5 | 22.928 % | c | 58843 | 32189 128877 | 15579 13918 917727 65.9 | 22.936 % | c | 59068 | 32189 128877 | 17137 14143 958504 67.8 | 22.936 % | c | 59405 | 32189 128877 | 18851 14480 1022609 70.6 | 22.936 % | c | 59914 | 32189 128877 | 20736 14989 1071923 71.5 | 22.936 % | c | 60673 | 32142 128720 | 22776 15745 1187821 75.4 | 22.978 % | c | 61812 | 32142 128720 | 25054 16884 1397967 82.8 | 22.978 % | c | 63520 | 31956 127065 | 27400 18586 1655422 89.1 | 23.171 % | c | 66082 | 31952 127053 | 30136 21138 2044209 96.7 | 23.179 % | c | 69927 | 31714 126257 | 32903 24970 2749424 110.1 | 23.490 % | c | 75694 | 31208 124124 | 35616 30709 4199777 136.8 | 24.043 % | c ============================================================================== c (current CPU-time: 271.244 s) c ============================================================================== c [1mFound solution: 1704[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 79985 | 31241 124250 | 9372 34954 4909549 140.5 | 24.043 % | c -- subsuming c -- var.elim.: 1000/1120 c -- var.elim.: 1120/1120 c -- var.elim.: 1000/1099 c -- var.elim.: 1099/1099 c -- var.elim.: 591/591 c -- var.elim.: 626/626 c -- var.elim.: 582/582 c -- var.elim.: 326/326 c -- subsuming c -- var.elim.: 601/601 c -- var.elim.: 29/29 c | 79985 | 30895 124299 | -- 34954 -- -- | -- | -342/58 c | 79985 | 30895 124299 | 12358 25895 1815691 70.1 | 24.043 % | c | 80085 | 30889 124278 | 13591 12897 708897 55.0 | 24.476 % | c | 80236 | 30889 124278 | 14950 13048 714058 54.7 | 24.476 % | c | 80462 | 30889 124278 | 16445 13274 742439 55.9 | 24.476 % | c | 80799 | 30889 124278 | 18089 13611 790500 58.1 | 24.476 % | c | 81307 | 30889 124278 | 19898 14119 806153 57.1 | 24.476 % | c | 82067 | 30889 124278 | 21888 14879 948295 63.7 | 24.476 % | c | 83209 | 30889 124278 | 24077 16021 1220457 76.2 | 24.476 % | c | 84918 | 30889 124278 | 26485 17730 1518536 85.6 | 24.476 % | c | 87480 | 30889 124278 | 29133 20292 2069775 102.0 | 24.476 % | c | 91326 | 30889 124278 | 32047 24138 2775961 115.0 | 24.476 % | c | 97092 | 30889 124278 | 35251 29904 3597056 120.3 | 24.476 % | c ============================================================================== c (current CPU-time: 366.447 s) c ============================================================================== c [1mFound solution: 1703[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 104034 | 31006 124640 | 9301 36843 5115014 138.8 | 24.476 % | c -- subsuming c -- var.elim.: 267/267 c -- var.elim.: 216/216 c -- var.elim.: 103/103 c -- var.elim.: 2/2 c | 104034 | 30878 124398 | -- 36843 -- -- | -- | -127/-239 c | 104034 | 30878 124398 | 12351 32685 3710751 113.5 | 24.476 % | c | 104135 | 30755 123921 | 13532 15205 1471765 96.8 | 24.612 % | c | 104286 | 30755 123921 | 14885 15356 1494458 97.3 | 24.612 % | c | 104512 | 30744 123859 | 16368 15578 1519916 97.6 | 24.654 % | c | 104850 | 30744 123859 | 18004 15916 1578494 99.2 | 24.654 % | c | 105356 | 30744 123859 | 19805 16422 1644182 100.1 | 24.654 % | c | 106115 | 30744 123859 | 21785 17181 1785308 103.9 | 24.654 % | c | 107254 | 30744 123859 | 23964 18320 1898677 103.6 | 24.654 % | c | 108962 | 30744 123859 | 26360 20028 2250995 112.4 | 24.654 % | c | 111525 | 30744 123859 | 28997 22591 2635346 116.7 | 24.654 % | c | 115370 | 30738 123838 | 31890 26435 3424205 129.5 | 24.663 % | c | 121136 | 30417 122575 | 34713 32178 4324932 134.4 | 25.061 % | c | 129785 | 30325 122083 | 38069 19968 2538414 127.1 | 25.163 % | c | 142761 | 30027 120406 | 41464 32938 6090613 184.9 | 25.503 % | c | 162222 | 29945 119722 | 45486 23365 3594317 153.8 | 25.587 % | c | 191415 | 29846 119415 | 49869 20541 3331169 162.2 | 25.731 % | c ============================================================================== c (current CPU-time: 790.107 s) c ============================================================================== c [1mFound solution: 1701[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 205392 | 29905 119657 | 8971 34495 7187571 208.4 | 25.731 % | c -- subsuming c -- var.elim.: 1000/1332 c -- var.elim.: 1332/1332 c -- var.elim.: 1000/1535 c -- var.elim.: 1535/1535 c -- var.elim.: 862/862 c -- var.elim.: 586/586 c -- subsuming c -- var.elim.: 883/883 c -- var.elim.: 32/32 c | 205392 | 29592 119055 | -- 34495 -- -- | -- | -311/-597 c | 205392 | 29592 119055 | 11836 20948 1446269 69.0 | 25.731 % | c | 205493 | 29592 119055 | 13020 9739 714047 73.3 | 26.127 % | c | 205644 | 29592 119055 | 14322 9890 724340 73.2 | 26.127 % | c | 205869 | 29592 119055 | 15754 10115 755412 74.7 | 26.127 % | c | 206206 | 29592 119055 | 17330 10452 816582 78.1 | 26.127 % | c | 206716 | 29592 119055 | 19063 10962 893083 81.5 | 26.127 % | c | 207478 | 29592 119055 | 20969 11724 972731 83.0 | 26.127 % | c | 208617 | 29587 119039 | 23062 12860 1147196 89.2 | 26.135 % | c ============================================================================== c (current CPU-time: 804.458 s) c ============================================================================== c [1mFound solution: 1693[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 209783 | 29685 119392 | 8905 14026 1362318 97.1 | 26.135 % | c -- subsuming c -- var.elim.: 240/240 c -- var.elim.: 199/199 c -- var.elim.: 74/74 c -- var.elim.: 44/44 c | 209783 | 29592 119263 | -- 14026 -- -- | -- | -91/-124 c | 209783 | 29592 119263 | 11836 13974 1353877 96.9 | 26.135 % | c | 209883 | 29592 119263 | 13020 14074 1358366 96.5 | 26.157 % | c | 210033 | 29592 119263 | 14322 14224 1375823 96.7 | 26.158 % | c | 210260 | 29592 119263 | 15754 14451 1415562 98.0 | 26.157 % | c | 210598 | 29592 119263 | 17330 14789 1471364 99.5 | 26.157 % | c | 211104 | 29592 119263 | 19063 15295 1552997 101.5 | 26.157 % | c | 211864 | 29592 119263 | 20969 16055 1665154 103.7 | 26.157 % | c | 213003 | 29592 119263 | 23066 17194 1908317 111.0 | 26.157 % | c | 214712 | 29592 119263 | 25373 18903 2135902 113.0 | 26.157 % | c | 217277 | 29592 119263 | 27910 21468 2681732 124.9 | 26.157 % | c | 221122 | 29587 119250 | 30696 25310 3477334 137.4 | 26.166 % | c | 226889 | 29587 119250 | 33766 31077 4882683 157.1 | 26.166 % | c ============================================================================== c (current CPU-time: 902.575 s) c ============================================================================== c [1mFound solution: 1680[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 235303 | 29761 119753 | 8928 18698 2969607 158.8 | 26.166 % | c -- subsuming c -- var.elim.: 319/319 c -- var.elim.: 230/230 c -- var.elim.: 166/166 c -- var.elim.: 110/110 c -- var.elim.: 108/108 c | 235303 | 29592 119379 | -- 18698 -- -- | -- | -167/-369 c | 235303 | 29592 119379 | 11836 18655 2961532 158.8 | 26.166 % | c | 235403 | 29592 119379 | 13020 12537 1549085 123.6 | 26.178 % | c | 235553 | 29592 119379 | 14322 12687 1561375 123.1 | 26.178 % | c | 235778 | 29592 119379 | 15754 12912 1587604 123.0 | 26.178 % | c | 236115 | 29592 119379 | 17330 13249 1625929 122.7 | 26.178 % | c | 236623 | 29592 119379 | 19063 13757 1699757 123.6 | 26.178 % | c | 237385 | 29592 119379 | 20969 14519 1801541 124.1 | 26.178 % | c | 238527 | 29592 119379 | 23066 15661 1979846 126.4 | 26.178 % | c | 240236 | 29592 119379 | 25373 17370 2216528 127.6 | 26.178 % | c | 242798 | 29592 119379 | 27910 19932 2682373 134.6 | 26.178 % | c | 246642 | 29581 119338 | 30690 23768 3107135 130.7 | 26.195 % | c | 252408 | 29581 119338 | 33759 29534 4279500 144.9 | 26.195 % | c ============================================================================== c (current CPU-time: 983.707 s) c ============================================================================== c [1mFound solution: 1676[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 257785 | 29680 119659 | 8903 34911 5312285 152.2 | 26.195 % | c -- subsuming c -- var.elim.: 234/234 c -- var.elim.: 177/177 c -- var.elim.: 121/121 c | 257785 | 29583 119464 | -- 34911 -- -- | -- | -97/-194 c | 257785 | 29583 119464 | 11833 32754 4860380 148.4 | 26.195 % | c | 257885 | 29572 119429 | 13011 10469 1297199 123.9 | 26.234 % | c | 258035 | 29572 119429 | 14312 10619 1312908 123.6 | 26.234 % | c | 258260 | 29572 119429 | 15744 10844 1323462 122.0 | 26.234 % | c | 258598 | 29572 119429 | 17318 11182 1371279 122.6 | 26.234 % | c | 259106 | 29572 119429 | 19050 11690 1414100 121.0 | 26.234 % | c | 259865 | 29566 119409 | 20951 12446 1518123 122.0 | 26.242 % | c | 261005 | 29566 119409 | 23046 13586 1584228 116.6 | 26.242 % | c ============================================================================== c (current CPU-time: 997.85 s) c ============================================================================== c [1mFound solution: 1674[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 262367 | 29710 119846 | 8912 14948 1811543 121.2 | 26.242 % | c -- subsuming c -- var.elim.: 279/279 c -- var.elim.: 209/209 c -- var.elim.: 148/148 c | 262367 | 29574 119633 | -- 14948 -- -- | -- | -135/-210 c | 262367 | 29574 119633 | 11829 14944 1811455 121.2 | 26.242 % | c | 262470 | 29574 119633 | 13012 10066 978874 97.2 | 26.248 % | c | 262620 | 29574 119633 | 14313 10216 989629 96.9 | 26.248 % | c | 262846 | 29574 119633 | 15745 10442 1018887 97.6 | 26.248 % | c | 263183 | 29569 119620 | 17316 10778 1060906 98.4 | 26.257 % | c | 263689 | 29569 119620 | 19048 11284 1141706 101.2 | 26.257 % | c | 264450 | 29569 119620 | 20953 12045 1273488 105.7 | 26.257 % | c | 265592 | 29569 119620 | 23048 13187 1510277 114.5 | 26.257 % | c ============================================================================== c (current CPU-time: 1013.45 s) c ============================================================================== c [1mFound solution: 1668[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 267291 | 29673 119992 | 8901 14886 1880053 126.3 | 26.257 % | c -- subsuming c -- var.elim.: 262/262 c -- var.elim.: 207/207 c -- var.elim.: 130/130 c | 267291 | 29576 119870 | -- 14886 -- -- | -- | -97/-121 c | 267291 | 29576 119870 | 11830 14886 1880053 126.3 | 26.257 % | c | 267391 | 29576 119870 | 13013 10024 1180970 117.8 | 26.266 % | c | 267542 | 29576 119870 | 14314 10175 1205346 118.5 | 26.266 % | c | 267775 | 29576 119870 | 15746 10408 1227816 118.0 | 26.266 % | c | 268113 | 29576 119870 | 17320 10746 1295927 120.6 | 26.266 % | c | 268620 | 29576 119870 | 19052 11253 1325933 117.8 | 26.266 % | c | 269379 | 29576 119870 | 20958 12012 1465321 122.0 | 26.266 % | c | 270520 | 29576 119870 | 23054 13153 1548742 117.7 | 26.266 % | c | 272229 | 29565 119834 | 25350 14859 1888396 127.1 | 26.283 % | c ============================================================================== c (current CPU-time: 1033.09 s) c ============================================================================== c [1mFound solution: 1667[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 273554 | 29707 120298 | 8912 16184 2134997 131.9 | 26.283 % | c -- subsuming c -- var.elim.: 314/314 c -- var.elim.: 235/235 c -- var.elim.: 143/143 c -- var.elim.: 111/111 c | 273554 | 29573 120392 | -- 16184 -- -- | -- | -133/97 c | 273554 | 29573 120392 | 11829 15694 2007220 127.9 | 26.283 % | c | 273655 | 29573 120392 | 13012 10564 1139654 107.9 | 26.300 % | c | 273806 | 29573 120392 | 14313 10715 1163193 108.6 | 26.300 % | c | 274031 | 29573 120392 | 15744 10940 1178101 107.7 | 26.300 % | c | 274369 | 29573 120392 | 17319 11278 1249635 110.8 | 26.300 % | c | 274875 | 29573 120392 | 19051 11784 1331954 113.0 | 26.300 % | c | 275634 | 29573 120392 | 20956 12543 1475191 117.6 | 26.300 % | c | 276773 | 29573 120392 | 23051 13682 1714801 125.3 | 26.300 % | c | 278484 | 29573 120392 | 25356 15393 2066557 134.3 | 26.300 % | c | 281046 | 29573 120392 | 27892 17955 2496483 139.0 | 26.300 % | c | 284891 | 29573 120392 | 30681 21800 3389005 155.5 | 26.300 % | c | 290657 | 29472 118843 | 33634 27562 4719645 171.2 | 26.403 % | c ============================================================================== c (current CPU-time: 1105.05 s) c ============================================================================== c [1mFound solution: 1656[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 294568 | 29572 119164 | 8871 31473 5545007 176.2 | 26.403 % | c -- subsuming c -- var.elim.: 664/664 c -- var.elim.: 696/696 c -- var.elim.: 87/87 c -- subsuming c -- var.elim.: 472/472 c -- var.elim.: 8/8 c | 294568 | 29460 120248 | -- 31473 -- -- | -- | -112/1085 c | 294568 | 29460 120248 | 11784 31434 5534395 176.1 | 26.403 % | c | 294668 | 29460 120248 | 12962 11195 1864412 166.5 | 26.457 % | c | 294818 | 29460 120248 | 14258 11345 1880068 165.7 | 26.457 % | c | 295043 | 29451 120220 | 15679 11569 1912658 165.3 | 26.465 % | c | 295382 | 29451 120220 | 17247 11908 1958515 164.5 | 26.465 % | c | 295888 | 29451 120220 | 18972 12414 2027680 163.3 | 26.465 % | c | 296649 | 29451 120220 | 20869 13175 2122412 161.1 | 26.465 % | c ============================================================================== c (current CPU-time: 1115.25 s) c ============================================================================== c [1mFound solution: 1655[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 297188 | 29587 120637 | 8876 13714 2236057 163.0 | 26.465 % | c -- subsuming c -- var.elim.: 273/273 c -- var.elim.: 233/233 c -- var.elim.: 113/113 c -- var.elim.: 64/64 c -- var.elim.: 63/63 c | 297188 | 29453 120346 | -- 13714 -- -- | -- | -134/-290 c | 297188 | 29453 120346 | 11781 13496 2094104 155.2 | 26.465 % | c | 297288 | 29453 120346 | 12959 13596 2095769 154.1 | 26.476 % | c | 297440 | 29440 120293 | 14248 13747 2107609 153.3 | 26.485 % | c | 297666 | 29440 1#### 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.82 0.92 0.90 2/55 3664 Raw data (stat): 3664 (runsolver) R 3663 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546961351 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0009 s] Raw data (loadavg): 0.92 0.93 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 4841 0 0 0 981 17 0 0 25 0 1 0 546961351 18628608 3911 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4548 3911 603 41 0 4507 0 vsize: 18192 [startup+20.0019 s] Raw data (loadavg): 0.93 0.94 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 7780 0 0 0 1967 29 0 0 25 0 1 0 546961351 18296832 3844 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4467 3844 603 41 0 4426 0 vsize: 17868 [startup+30.0032 s] Raw data (loadavg): 0.94 0.94 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 9556 0 0 0 2961 36 0 0 25 0 1 0 546961351 19132416 4052 4294967295 134512640 134672761 3221224544 3221223460 1075349617 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4671 4052 603 41 0 4630 0 vsize: 18684 [startup+40.0044 s] Raw data (loadavg): 0.95 0.94 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 10862 0 0 0 3954 43 0 0 25 0 1 0 546961351 19611648 4160 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4788 4160 603 41 0 4747 0 vsize: 19152 [startup+50.0046 s] Raw data (loadavg): 0.96 0.94 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 11357 0 0 0 4953 44 0 0 25 0 1 0 546961351 21721088 4655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5303 4655 603 41 0 5262 0 vsize: 21212 [startup+60.0059 s] Raw data (loadavg): 0.96 0.94 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 12362 0 0 0 5948 49 0 0 25 0 1 0 546961351 23363584 5079 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5704 5079 603 41 0 5663 0 vsize: 22816 [startup+70.0069 s] Raw data (loadavg): 0.97 0.94 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 12362 0 0 0 6948 49 0 0 25 0 1 0 546961351 23363584 5079 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5704 5079 603 41 0 5663 0 vsize: 22816 [startup+80.0083 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 12852 0 0 0 7947 50 0 0 25 0 1 0 546961351 25464832 5569 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6217 5569 603 41 0 6176 0 vsize: 24868 [startup+90.0087 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 13484 0 0 0 8945 53 0 0 25 0 1 0 546961351 27975680 6201 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6830 6201 603 41 0 6789 0 vsize: 27320 [startup+100.009 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 14025 0 0 0 9943 54 0 0 25 0 1 0 546961351 30212096 6742 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7376 6742 603 41 0 7335 0 vsize: 29504 [startup+110.01 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 14467 0 0 0 10942 56 0 0 25 0 1 0 546961351 32067584 7184 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7829 7184 603 41 0 7788 0 vsize: 31316 [startup+120.01 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 15356 0 0 0 11939 59 0 0 25 0 1 0 546961351 34242560 7675 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8360 7675 603 41 0 8319 0 vsize: 33440 [startup+130.011 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 15724 0 0 0 12936 62 0 0 25 0 1 0 546961351 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8263 7648 603 41 0 8222 0 vsize: 33052 [startup+140.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3664 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 15724 0 0 0 13936 63 0 0 25 0 1 0 546961351 33845248 7648 4294967295 134512640 134672761 3221224544 3221223680 134614524 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8263 7648 603 41 0 8222 0 vsize: 33052 [startup+150.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 15724 0 0 0 14935 63 0 0 25 0 1 0 546961351 33845248 7648 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8263 7648 603 41 0 8222 0 vsize: 33052 [startup+160.013 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 15724 0 0 0 15935 63 0 0 25 0 1 0 546961351 33845248 7648 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8263 7648 603 41 0 8222 0 vsize: 33052 [startup+170.014 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 15724 0 0 0 16935 64 0 0 25 0 1 0 546961351 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8263 7648 603 41 0 8222 0 vsize: 33052 [startup+180.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 15724 0 0 0 17935 64 0 0 25 0 1 0 546961351 33845248 7648 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8263 7648 603 41 0 8222 0 vsize: 33052 [startup+190.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 16696 0 0 0 18931 68 0 0 25 0 1 0 546961351 36438016 8220 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8896 8220 603 41 0 8855 0 vsize: 35584 [startup+200.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 17090 0 0 0 19928 71 0 0 25 0 1 0 546961351 36630528 8282 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8943 8282 603 41 0 8902 0 vsize: 35772 [startup+210.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 17090 0 0 0 20928 71 0 0 25 0 1 0 546961351 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8943 8282 603 41 0 8902 0 vsize: 35772 [startup+220.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 17090 0 0 0 21928 71 0 0 25 0 1 0 546961351 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8943 8282 603 41 0 8902 0 vsize: 35772 [startup+230.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 17090 0 0 0 22928 71 0 0 25 0 1 0 546961351 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8943 8282 603 41 0 8902 0 vsize: 35772 [startup+240.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 17090 0 0 0 23928 71 0 0 25 0 1 0 546961351 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8943 8282 603 41 0 8902 0 vsize: 35772 [startup+250.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 17090 0 0 0 24928 72 0 0 25 0 1 0 546961351 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8943 8282 603 41 0 8902 0 vsize: 35772 [startup+260.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 17090 0 0 0 25927 72 0 0 25 0 1 0 546961351 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8943 8282 603 41 0 8902 0 vsize: 35772 [startup+270.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 17455 0 0 0 26926 73 0 0 25 0 1 0 546961351 38076416 8647 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9296 8647 603 41 0 9255 0 vsize: 37184 [startup+280.022 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 27922 78 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+290.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 28921 78 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 29921 79 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 30921 79 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+320.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 31921 80 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 32921 80 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+340.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 33920 80 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+350.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 34920 80 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+360.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 18329 0 0 0 35920 81 0 0 25 0 1 0 546961351 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9826 9115 603 41 0 9785 0 vsize: 39304 [startup+370.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 36917 84 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+380.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 37917 84 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+390.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 38917 84 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+400.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 39916 85 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+410.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 40916 85 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+420.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 41916 85 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+430.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 42916 85 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+440.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3666 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 43916 85 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+450.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19008 0 0 0 44915 87 0 0 25 0 1 0 546961351 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10141 9412 603 41 0 10100 0 vsize: 40564 [startup+460.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19134 0 0 0 45914 88 0 0 25 0 1 0 546961351 41668608 9538 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10173 9538 603 41 0 10132 0 vsize: 40692 [startup+470.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19325 0 0 0 46913 88 0 0 25 0 1 0 546961351 42291200 9691 4294967295 134512640 134672761 3221224544 3221223688 134616314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10325 9691 603 41 0 10284 0 vsize: 41300 [startup+480.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19325 0 0 0 47913 89 0 0 25 0 1 0 546961351 42291200 9691 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10325 9691 603 41 0 10284 0 vsize: 41300 [startup+490.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19325 0 0 0 48912 89 0 0 25 0 1 0 546961351 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10325 9691 603 41 0 10284 0 vsize: 41300 [startup+500.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19325 0 0 0 49912 89 0 0 25 0 1 0 546961351 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10325 9691 603 41 0 10284 0 vsize: 41300 [startup+510.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19338 0 0 0 50913 89 0 0 25 0 1 0 546961351 42426368 9704 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10358 9704 603 41 0 10317 0 vsize: 41432 [startup+520.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 19858 0 0 0 51911 91 0 0 25 0 1 0 546961351 44527616 10224 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10871 10224 603 41 0 10830 0 vsize: 43484 [startup+530.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 20419 0 0 0 52910 92 0 0 25 0 1 0 546961351 46895104 10785 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11449 10785 603 41 0 11408 0 vsize: 45796 [startup+540.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 20880 0 0 0 53909 94 0 0 25 0 1 0 546961351 48726016 11246 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11896 11246 603 41 0 11855 0 vsize: 47584 [startup+550.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 21306 0 0 0 54907 95 0 0 25 0 1 0 546961351 50434048 11672 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12313 11672 603 41 0 12272 0 vsize: 49252 [startup+560.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 21684 0 0 0 55906 96 0 0 25 0 1 0 546961351 52031488 12050 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12703 12050 603 41 0 12662 0 vsize: 50812 [startup+570.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22163 0 0 0 56904 98 0 0 25 0 1 0 546961351 54009856 12529 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13186 12529 603 41 0 13145 0 vsize: 52744 [startup+580.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22756 0 0 0 57902 101 0 0 25 0 1 0 546961351 56377344 13122 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13764 13122 603 41 0 13723 0 vsize: 55056 [startup+590.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 58901 102 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+600.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 59900 102 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+610.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 60900 103 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+620.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 61900 103 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223564 134565024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+630.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 62900 103 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+640.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 63900 103 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+650.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 64900 104 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+660.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 65899 104 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+670.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 66899 105 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+680.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 67899 105 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+690.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 68899 105 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+700.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22945 0 0 0 69899 105 0 0 25 0 1 0 546961351 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13265 603 41 0 13851 0 vsize: 55568 [startup+710.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22946 0 0 0 70898 106 0 0 25 0 1 0 546961351 56901632 13266 4294967295 134512640 134672761 3221224544 3221223556 134565028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13266 603 41 0 13851 0 vsize: 55568 [startup+720.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 22948 0 0 0 71898 106 0 0 25 0 1 0 546961351 56901632 13268 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 13268 603 41 0 13851 0 vsize: 55568 [startup+730.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 23074 0 0 0 72898 107 0 0 25 0 1 0 546961351 57339904 13376 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13999 13376 603 41 0 13958 0 vsize: 55996 [startup+740.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3668 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 23074 0 0 0 73897 107 0 0 25 0 1 0 546961351 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13999 13376 603 41 0 13958 0 vsize: 55996 [startup+750.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 23074 0 0 0 74897 107 0 0 25 0 1 0 546961351 57339904 13376 4294967295 134512640 134672761 3221224544 3221223584 134612653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13999 13376 603 41 0 13958 0 vsize: 55996 [startup+760.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 23074 0 0 0 75897 108 0 0 25 0 1 0 546961351 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13999 13376 603 41 0 13958 0 vsize: 55996 [startup+770.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 23074 0 0 0 76897 108 0 0 25 0 1 0 546961351 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13999 13376 603 41 0 13958 0 vsize: 55996 [startup+780.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 23074 0 0 0 77897 108 0 0 25 0 1 0 546961351 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13999 13376 603 41 0 13958 0 vsize: 55996 [startup+790.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 23074 0 0 0 78897 109 0 0 25 0 1 0 546961351 57339904 13376 4294967295 134512640 134672761 3221224544 3221223584 134613818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13999 13376 603 41 0 13958 0 vsize: 55996 [startup+800.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 23948 0 0 0 79893 112 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+810.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 80891 115 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223680 134614685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+820.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 81891 115 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+830.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 82890 115 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+840.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 83890 115 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+850.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 84890 116 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+860.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 85889 116 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+870.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 86889 117 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+880.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 87889 117 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+890.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24332 0 0 0 88889 117 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+900.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24369 0 0 0 89888 118 0 0 25 0 1 0 546961351 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13415 603 41 0 14019 0 vsize: 56240 [startup+910.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24765 0 0 0 90886 120 0 0 25 0 1 0 546961351 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13419 603 41 0 14019 0 vsize: 56240 [startup+920.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24765 0 0 0 91886 120 0 0 25 0 1 0 546961351 57589760 13419 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13419 603 41 0 14019 0 vsize: 56240 [startup+930.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24765 0 0 0 92886 121 0 0 25 0 1 0 546961351 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13419 603 41 0 14019 0 vsize: 56240 [startup+940.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24765 0 0 0 93886 121 0 0 25 0 1 0 546961351 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13419 603 41 0 14019 0 vsize: 56240 [startup+950.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24765 0 0 0 94886 121 0 0 25 0 1 0 546961351 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13419 603 41 0 14019 0 vsize: 56240 [startup+960.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24765 0 0 0 95886 121 0 0 25 0 1 0 546961351 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13419 603 41 0 14019 0 vsize: 56240 [startup+970.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24765 0 0 0 96886 122 0 0 25 0 1 0 546961351 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13419 603 41 0 14019 0 vsize: 56240 [startup+980.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 24765 0 0 0 97885 122 0 0 25 0 1 0 546961351 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13419 603 41 0 14019 0 vsize: 56240 [startup+990.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 25162 0 0 0 98882 125 0 0 25 0 1 0 546961351 57589760 13421 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14060 13421 603 41 0 14019 0 vsize: 56240 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3670 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 25559 0 0 0 99878 129 0 0 25 0 1 0 546961351 57540608 13409 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13409 603 41 0 14007 0 vsize: 56192 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/59 3674 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 25559 0 0 0 100875 133 0 0 25 0 1 0 546961351 57540608 13409 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14048 13409 603 41 0 14007 0 vsize: 56192 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3723 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 25965 0 0 0 101868 139 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3723 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 25965 0 0 0 102868 139 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3723 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 26315 0 0 0 103865 142 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3725 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 26315 0 0 0 104865 142 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3725 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 26315 0 0 0 105865 143 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3725 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 26315 0 0 0 106865 143 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 26315 0 0 0 107865 143 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 26315 0 0 0 108865 143 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 26315 0 0 0 109865 143 0 0 25 0 1 0 546961351 57540608 13411 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13411 603 41 0 14007 0 vsize: 56192 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 26726 0 0 0 110862 146 0 0 25 0 1 0 546961351 57540608 13418 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14048 13418 603 41 0 14007 0 vsize: 56192 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 111859 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 [startup+1130.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 112859 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 [startup+1140.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 113859 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 114860 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 [startup+1160.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 115860 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 116860 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 117860 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 118860 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 3727 Raw data (stat): 3664 (minisat+) R 3663 20024 20023 0 -1 0 27079 0 0 0 119861 149 0 0 25 0 1 0 546961351 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14048 13420 603 41 0 14007 0 vsize: 56192 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 1/55 3727 Raw data (stat): 3664 (minisat+) Z 3663 20024 20023 0 -1 12 27080 0 0 0 119861 152 0 0 25 0 1 0 546961351 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.1 CPU time (s): 1200.13 CPU user time (s): 1198.61 CPU system time (s): 1.52277 CPU usage (%): 100.003 Max. virtual memory (Kb): 56240 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####