Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0282.opb |
MD5SUM | a733e9fa1e4e3ac90baf85249f7c3e9a |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 258411 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 282 |
Biggest coefficient in the objective function | 160646 |
Number of bits for the biggest coefficient in the objective function | 18 |
Sum of the numbers in the objective function | 1302615 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 160646 |
Number of bits of the biggest number in a constraint | 18 |
Biggest sum of numbers in a constraint | 1302615 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.01984 |
Number of variables | 282 |
Total number of constraints | 523 |
Number of constraints which are clauses | 177 |
Number of constraints which are cardinality constraints (but not clauses) | 282 |
Number of constraints which are nor clauses,nor cardinality constraints | 64 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 57 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-04-21 09:13:02 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12141 boxname=wulflinc22 idbench=934 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a733e9fa1e4e3ac90baf85249f7c3e9a /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-p0282.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-p0282.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-p0282.opb IDLAUNCH: 12141 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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: 536344 kB Buffers: 31784 kB Cached: 436236 kB SwapCached: 24 kB Active: 151936 kB Inactive: 318760 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 536092 kB SwapTotal: 2097892 kB SwapFree: 2097660 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6640 kB Slab: 21896 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 09:33:04 (client local time) WITH STATUS 10 IN 1200.22 SECONDS stats: 12141 7 1200.22 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 221 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): sss................................................................................................................................................................................. c ---[ 223]---> BDD-cost: 580 c ---[ 222]---> BDD-cost: 587 c ---[ 221]---> BDD-cost: 540 c ---[ 220]---> BDD-cost: 394 c ---[ 219]---> BDD-cost: 497 c ---[ 218]---> BDD-cost: 370 c ---[ 217]---> BDD-cost: 386 c ---[ 216]---> BDD-cost: 415 c ---[ 215]---> BDD-cost: 348 c ---[ 214]---> BDD-cost: 385 c ---[ 213]---> BDD-cost: 744 c ---[ 211]---> BDD-cost: 791 c ---[ 209]---> BDD-cost: 828 c ---[ 208]---> BDD-cost: 473 c ---[ 207]---> BDD-cost: 492 c ---[ 206]---> BDD-cost: 528 c ---[ 205]---> BDD-cost: 310 c ---[ 204]---> BDD-cost: 347 c ---[ 203]---> BDD-cost: 219 c ---[ 202]---> BDD-cost: 267 c ---[ 201]---> BDD-cost: 593 c ---[ 199]---> BDD-cost: 396 c ---[ 198]---> BDD-cost: 448 c ---[ 197]---> BDD-cost: 323 c ---[ 196]---> BDD-cost: 369 c ---[ 195]---> BDD-cost: 578 c ---[ 194]---> BDD-cost: 602 c ---[ 193]---> BDD-cost: 659 c ---[ 192]---> BDD-cost: 350 c ---[ 191]---> BDD-cost: 872 c ---[ 190]---> BDD-cost: 362 c ---[ 189]---> BDD-cost: 897 c ---[ 188]---> BDD-cost: 423 c ---[ 187]---> BDD-cost: 56 c ---[ 186]---> BDD-cost: 10 c ---[ 185]---> BDD-cost: 56 c ---[ 184]---> BDD-cost: 56 c ---[ 183]---> BDD-cost: 16 c ---[ 182]---> BDD-cost: 26 c ---[ 181]---> BDD-cost: 8 c ---[ 180]---> BDD-cost: 4 c ---[ 2]---> BDD-cost: 87 c ---[ 1]---> BDD-cost: 143 c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 41898 123412 | 13966 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 513010[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:77326 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 259193 631180 | 86397 0 0 nan | 0.000 % | c | 101 | 259155 631099 | 95036 98 3620 36.9 | 0.064 % | c | 251 | 259139 631065 | 104540 247 4873 19.7 | 0.069 % | c | 478 | 259124 631032 | 114994 473 6580 13.9 | 0.073 % | c | 815 | 259124 631032 | 126493 810 8587 10.6 | 0.073 % | c | 1321 | 259099 630977 | 139143 1314 13473 10.3 | 0.081 % | c | 2081 | 258740 630169 | 153057 2065 21521 10.4 | 0.191 % | c ============================================================================== c [1mFound solution: 498997[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2156 | 259176 631678 | 86392 2136 22949 10.7 | 0.191 % | c ============================================================================== c [1mFound solution: 494881[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2205 | 261090 636467 | 87030 2185 25546 11.7 | 0.191 % | c | 2305 | 261090 636467 | 95733 2285 26048 11.4 | 0.223 % | c | 2455 | 261084 636455 | 105306 2434 29181 12.0 | 0.227 % | c | 2680 | 261020 636313 | 115836 2656 31234 11.8 | 0.245 % | c ============================================================================== c [1mFound solution: 489052[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2929 | 260996 636263 | 86998 2900 37163 12.8 | 0.245 % | c | 3029 | 260996 636263 | 95697 3000 38487 12.8 | 0.257 % | c | 3184 | 260996 636263 | 105267 3155 41943 13.3 | 0.257 % | c | 3409 | 260996 636263 | 115794 3380 46827 13.9 | 0.257 % | c | 3746 | 260984 636236 | 127373 3716 51764 13.9 | 0.260 % | c | 4252 | 260744 635700 | 140111 4216 58764 13.9 | 0.328 % | c ============================================================================== c [1mFound solution: 476792[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4639 | 261607 638147 | 87202 4597 65258 14.2 | 0.328 % | c | 4739 | 261607 638147 | 95922 4697 66637 14.2 | 0.387 % | c | 4891 | 261599 638131 | 105514 4848 69883 14.4 | 0.391 % | c | 5117 | 261265 637377 | 116065 5015 72749 14.5 | 0.494 % | c | 5455 | 261153 637126 | 127672 5351 97792 18.3 | 0.530 % | c | 5961 | 261134 637088 | 140439 5855 107474 18.4 | 0.540 % | c | 6723 | 261021 636832 | 154483 6607 114145 17.3 | 0.578 % | c ============================================================================== c [1mFound solution: 467587[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7001 | 261035 636870 | 87011 6884 118219 17.2 | 0.578 % | c | 7101 | 261035 636870 | 95712 6984 118768 17.0 | 0.581 % | c | 7252 | 261035 636870 | 105283 7135 119612 16.8 | 0.581 % | c | 7479 | 260920 636614 | 115811 7354 126675 17.2 | 0.619 % | c | 7816 | 260920 636614 | 127392 7691 132194 17.2 | 0.619 % | c | 8322 | 260920 636614 | 140132 8197 136987 16.7 | 0.619 % | c | 9082 | 260781 636299 | 154145 8950 145188 16.2 | 0.663 % | c | 10222 | 260781 636299 | 169559 10090 163514 16.2 | 0.663 % | c | 11930 | 260761 636254 | 186515 11797 203194 17.2 | 0.668 % | c | 14495 | 260761 636254 | 205167 14362 283870 19.8 | 0.668 % | c | 18339 | 260629 635955 | 225684 18171 377969 20.8 | 0.707 % | c ============================================================================== c [1mFound solution: 467586[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21468 | 260976 636813 | 86992 21297 478405 22.5 | 0.707 % | c | 21569 | 260976 636813 | 95691 21398 478954 22.4 | 0.714 % | c | 21719 | 260976 636813 | 105260 21548 482573 22.4 | 0.714 % | c | 21946 | 260976 636813 | 115786 21775 484743 22.3 | 0.714 % | c | 22283 | 260976 636813 | 127364 22112 489498 22.1 | 0.714 % | c | 22789 | 260976 636813 | 140101 22618 493010 21.8 | 0.714 % | c | 23549 | 260976 636813 | 154111 23378 530738 22.7 | 0.714 % | c | 24688 | 260976 636813 | 169522 24517 549168 22.4 | 0.714 % | c ============================================================================== c [1mFound solution: 467532[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26257 | 260882 636798 | 86960 26083 636622 24.4 | 0.714 % | c | 26357 | 260882 636798 | 95656 26183 638086 24.4 | 0.750 % | c | 26507 | 260882 636798 | 105221 26333 639047 24.3 | 0.750 % | c | 26732 | 260882 636798 | 115743 26558 641632 24.2 | 0.750 % | c | 27069 | 260850 636726 | 127318 26891 643701 23.9 | 0.759 % | c | 27575 | 260731 636457 | 140049 27392 678269 24.8 | 0.794 % | c | 28337 | 260680 636355 | 154054 28148 751900 26.7 | 0.821 % | c | 29477 | 260680 636355 | 169460 29288 771207 26.3 | 0.821 % | c | 31185 | 260261 635403 | 186406 30951 792866 25.6 | 0.955 % | c ============================================================================== c [1mFound solution: 467181[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31818 | 260268 635423 | 86756 31584 808504 25.6 | 0.955 % | c | 31918 | 260164 635187 | 95431 31682 809278 25.5 | 0.986 % | c | 32069 | 260164 635187 | 104974 31833 810098 25.4 | 0.986 % | c ============================================================================== c [1mFound solution: 416148[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32194 | 260182 635428 | 86727 31958 813972 25.5 | 0.986 % | c | 32296 | 260166 635396 | 95399 32059 815997 25.5 | 0.996 % | c | 32448 | 260067 635173 | 104939 32176 820443 25.5 | 1.025 % | c ============================================================================== c [1mFound solution: 397360[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32537 | 260074 635188 | 86691 32265 825831 25.6 | 1.025 % | c | 32639 | 260074 635188 | 95360 32367 826753 25.5 | 1.026 % | c | 32789 | 260074 635188 | 104896 32517 828781 25.5 | 1.026 % | c | 33014 | 260034 635098 | 115385 32740 830243 25.4 | 1.038 % | c | 33354 | 260034 635098 | 126924 33080 844043 25.5 | 1.038 % | c | 33860 | 259805 634578 | 139616 33569 849366 25.3 | 1.119 % | c | 34619 | 259715 634373 | 153578 34324 860826 25.1 | 1.149 % | c ============================================================================== c [1mFound solution: 397197[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35604 | 259582 634080 | 86527 35085 904152 25.8 | 1.149 % | c | 35706 | 259582 634080 | 95179 35187 905576 25.7 | 1.198 % | c | 35856 | 259306 633454 | 104697 35277 919906 26.1 | 1.287 % | c | 36081 | 259301 633444 | 115167 35501 932688 26.3 | 1.290 % | c | 36419 | 259275 633392 | 126684 35836 945651 26.4 | 1.304 % | c | 36925 | 259261 633364 | 139352 36340 982345 27.0 | 1.312 % | c | 37686 | 259253 633348 | 153287 37099 1006608 27.1 | 1.316 % | c | 38825 | 259019 632824 | 168616 38175 1033078 27.1 | 1.393 % | c | 40534 | 259000 632786 | 185478 39882 1082583 27.1 | 1.403 % | c ============================================================================== c [1mFound solution: 392796[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41981 | 258785 632307 | 86261 41144 1137670 27.7 | 1.403 % | c | 42081 | 258785 632307 | 94887 41244 1138188 27.6 | 1.478 % | c | 42231 | 258785 632307 | 104375 41394 1143754 27.6 | 1.478 % | c | 42456 | 258779 632295 | 114813 41618 1153246 27.7 | 1.481 % | c | 42793 | 258779 632295 | 126294 41955 1179844 28.1 | 1.481 % | c | 43299 | 258779 632295 | 138924 42461 1184039 27.9 | 1.481 % | c | 44058 | 258779 632295 | 152816 43220 1269904 29.4 | 1.481 % | c ============================================================================== c [1mFound solution: 392794[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 44949 | 258789 632325 | 86263 44111 1320493 29.9 | 1.481 % | c | 45049 | 258789 632325 | 94889 44211 1321370 29.9 | 1.482 % | c | 45199 | 258755 632247 | 104378 44358 1323938 29.8 | 1.493 % | c | 45425 | 258755 632247 | 114816 44584 1337792 30.0 | 1.493 % | c ============================================================================== c [1mFound solution: 392793[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45627 | 258765 632277 | 86255 44786 1357005 30.3 | 1.493 % | c | 45728 | 258765 632277 | 94880 44887 1357995 30.3 | 1.494 % | c | 45878 | 258765 632277 | 104368 45037 1358984 30.2 | 1.494 % | c | 46103 | 258761 632269 | 114805 45261 1362350 30.1 | 1.496 % | c ============================================================================== c [1mFound solution: 374086[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46345 | 258768 632288 | 86256 45502 1379989 30.3 | 1.496 % | c | 46445 | 258768 632288 | 94881 45602 1380818 30.3 | 1.502 % | c | 46595 | 258768 632288 | 104369 45752 1382275 30.2 | 1.502 % | c | 46822 | 258768 632288 | 114806 45979 1395722 30.4 | 1.502 % | c | 47161 | 258747 632246 | 126287 46315 1408436 30.4 | 1.513 % | c | 47668 | 258710 632169 | 138916 46815 1426244 30.5 | 1.528 % | c | 48427 | 258675 632088 | 152807 47571 1435198 30.2 | 1.540 % | c | 49568 | 258675 632088 | 168088 48712 1479350 30.4 | 1.540 % | c | 51277 | 258657 632052 | 184897 50419 1567140 31.1 | 1.550 % | c ============================================================================== c [1mFound solution: 357831[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51793 | 258550 631822 | 86183 50893 1588490 31.2 | 1.550 % | c | 51895 | 258550 631822 | 94801 50995 1589403 31.2 | 1.596 % | c | 52045 | 258550 631822 | 104281 51145 1601493 31.3 | 1.596 % | c ============================================================================== c [1mFound solution: 357615[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 52195 | 258559 631847 | 86186 51295 1619191 31.6 | 1.596 % | c | 52295 | 258559 631847 | 94804 51395 1621879 31.6 | 1.597 % | c | 52446 | 258559 631847 | 104285 51546 1622727 31.5 | 1.597 % | c | 52672 | 258559 631847 | 114713 51772 1639746 31.7 | 1.597 % | c | 53010 | 258559 631847 | 126184 52110 1676953 32.2 | 1.597 % | c | 53516 | 258559 631847 | 138803 52616 1708554 32.5 | 1.597 % | c | 54275 | 258559 631847 | 152683 53375 1728919 32.4 | 1.597 % | c | 55417 | 258559 631847 | 167952 54517 1772591 32.5 | 1.597 % | c ============================================================================== c [1mFound solution: 357593[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 55733 | 258574 632077 | 86191 54833 1797621 32.8 | 1.597 % | c | 55834 | 258574 632077 | 94810 54934 1799112 32.8 | 1.598 % | c | 55984 | 258574 632077 | 104291 55084 1800225 32.7 | 1.598 % | c | 56209 | 258574 632077 | 114720 55309 1804322 32.6 | 1.598 % | c | 56546 | 258574 632077 | 126192 55646 1822043 32.7 | 1.598 % | c | 57052 | 258574 632077 | 138811 56152 1826483 32.5 | 1.598 % | c | 57812 | 258368 631609 | 152692 56905 1861025 32.7 | 1.657 % | c | 58952 | 258368 631609 | 167961 58045 1955617 33.7 | 1.657 % | c ============================================================================== c [1mFound solution: 357592[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 59279 | 258368 631616 | 86122 58371 1972295 33.8 | 1.657 % | c | 59379 | 258302 631467 | 94734 58470 1973365 33.8 | 1.685 % | c | 59531 | 258302 631467 | 104207 58622 1980332 33.8 | 1.685 % | c | 59756 | 258302 631467 | 114628 58847 1987941 33.8 | 1.685 % | c | 60094 | 258286 631435 | 126091 59183 2017275 34.1 | 1.694 % | c | 60602 | 258280 631423 | 138700 59690 2060743 34.5 | 1.697 % | c | 61362 | 258147 631118 | 152570 60442 2075956 34.3 | 1.747 % | c | 62501 | 258147 631118 | 167827 61581 2207444 35.8 | 1.747 % | c | 64209 | 258147 631118 | 184610 63289 2399678 37.9 | 1.747 % | c | 66772 | 258141 631106 | 203071 65851 2498520 37.9 | 1.749 % | c | 70616 | 258141 631106 | 223378 69695 2740735 39.3 | 1.749 % | c | 76384 | 258119 631056 | 245716 75460 2861887 37.9 | 1.755 % | c ============================================================================== c [1mFound solution: 356984[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 76768 | 258133 631093 | 86044 75844 2869388 37.8 | 1.755 % | c | 76868 | 258133 631093 | 94648 75944 2870090 37.8 | 1.756 % | c | 77020 | 258133 631093 | 104113 76096 2871039 37.7 | 1.756 % | c | 77246 | 258133 631093 | 114524 76322 2872290 37.6 | 1.756 % | c ============================================================================== c [1mFound solution: 353456[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 77410 | 258140 631115 | 86046 76486 2880896 37.7 | 1.756 % | c ============================================================================== c [1mFound solution: 353455[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 77489 | 258147 631133 | 86049 76565 2882170 37.6 | 1.756 % | c | 77589 | 258147 631133 | 94653 76665 2886845 37.7 | 1.758 % | c | 77741 | 258147 631133 | 104119 76817 2895212 37.7 | 1.758 % | c | 77966 | 258147 631133 | 114531 77042 2917655 37.9 | 1.758 % | c | 78303 | 258133 631105 | 125984 77378 2942805 38.0 | 1.764 % | c | 78809 | 258129 631097 | 138582 77883 2981995 38.3 | 1.766 % | c | 79569 | 258129 631097 | 152441 78643 3027838 38.5 | 1.766 % | c ============================================================================== c [1mFound solution: 352971[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 79610 | 258139 631124 | 86046 78684 3029287 38.5 | 1.766 % | c ============================================================================== c [1mFound solution: 352970[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 79652 | 258149 631152 | 86049 78726 3033329 38.5 | 1.766 % | c | 79752 | 258149 631152 | 94653 78826 3036444 38.5 | 1.768 % | c | 79902 | 258149 631152 | 104119 78976 3047309 38.6 | 1.768 % | c | 80127 | 258149 631152 | 114531 79201 3065589 38.7 | 1.768 % | c | 80466 | 258149 631152 | 125984 79540 3098858 39.0 | 1.768 % | c | 80972 | 258149 631152 | 138582 80046 3136188 39.2 | 1.768 % | c | 81731 | 258149 631152 | 152441 80805 3264922 40.4 | 1.768 % | c | 82870 | 258145 631144 | 167685 81943 3333338 40.7 | 1.770 % | c | 84578 | 258141 631136 | 184453 83650 3569773 42.7 | 1.772 % | c | 87140 | 258141 631136 | 202899 86212 3850183 44.7 | 1.772 % | c | 90984 | 258141 631136 | 223188 90056 4371306 48.5 | 1.772 % | c ============================================================================== c [1mFound solution: 352969[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 94738 | 258139 631140 | 86046 93809 4816374 51.3 | 1.772 % | c | 94841 | 258139 631140 | 94650 26654 1588476 59.6 | 1.780 % | c | 94991 | 258139 631140 | 104115 26804 1595613 59.5 | 1.780 % | c ============================================================================== c [1mFound solution: 331113[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 95154 | 258152 631171 | 86050 26967 1597361 59.2 | 1.780 % | c | 95255 | 258152 631171 | 94655 27068 1597893 59.0 | 1.781 % | c | 95406 | 258152 631171 | 104120 27219 1617892 59.4 | 1.781 % | c | 95632 | 258145 631157 | 114532 27444 1633120 59.5 | 1.784 % | c | 95969 | 258138 631143 | 125985 27780 1653086 59.5 | 1.787 % | c | 96476 | 258138 631143 | 138584 28287 1674392 59.2 | 1.787 % | c | 97235 | 258138 631143 | 152442 29046 1708620 58.8 | 1.787 % | c | 98375 | 258138 631143 | 167687 30186 1789788 59.3 | 1.787 % | c | 100087 | 258138 631143 | 184455 31898 1905905 59.7 | 1.787 % | c ============================================================================== c [1mFound solution: 330534[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 102099 | 258141 631152 | 86047 33908 2049525 60.4 | 1.787 % | c | 102201 | 258141 631152 | 94651 34010 2050464 60.3 | 1.791 % | c | 102351 | 258141 631152 | 104116 34160 2054690 60.1 | 1.791 % | c | 102576 | 258141 631152 | 114528 34385 2064233 60.0 | 1.791 % | c | 102914 | 258132 631134 | 125981 34721 2096107 60.4 | 1.795 % | c | 103420 | 258123 631116 | 138579 35225 2138135 60.7 | 1.799 % | c | 104180 | 258123 631116 | 152437 35985 2168832 60.3 | 1.799 % | c | 105320 | 258123 631116 | 167681 37125 2265246 61.0 | 1.799 % | c | 107028 | 258123 631116 | 184449 38833 2578414 66.4 | 1.799 % | c | 109591 | 258105 631080 | 202894 41395 2715872 65.6 | 1.808 % | c ============================================================================== c [1mFound solution: 330532[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 110485 | 258116 631107 | 86038 42289 2828505 66.9 | 1.808 % | c | 110586 | 258099 631073 | 94641 42389 2840524 67.0 | 1.818 % | c | 110736 | 258088 631051 | 104105 42536 2846739 66.9 | 1.822 % | c | 110964 | 258088 631051 | 114516 42764 2848455 66.6 | 1.822 % | c | 111301 | 258088 631051 | 125968 43101 2852967 66.2 | 1.822 % | c | 111808 | 258088 631051 | 138565 43608 2867535 65.8 | 1.822 % | c ============================================================================== c [1mFound solution: 330344[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 112455 | 258096 631071 | 86032 44254 2898369 65.5 | 1.822 % | c | 112555 | 258096 631071 | 94635 44354 2898888 65.4 | 1.825 % | c | 112705 | 258090 631059 | 104098 44503 2907865 65.3 | 1.828 % | c | 112930 | 258086 631051 | 114508 44727 2920418 65.3 | 1.830 % | c | 113270 | 258086 631051 | 125959 45067 2944898 65.3 | 1.830 % | c | 113778 | 258086 631051 | 138555 45575 2997382 65.8 | 1.830 % | c | 114541 | 258058 630995 | 152410 46335 3026520 65.3 | 1.844 % | c | 115680 | 258032 630943 | 167652 47470 3094584 65.2 | 1.856 % | c | 117388 | 258023 630925 | 184417 49177 3249344 66.1 | 1.861 % | c ============================================================================== c [1mFound solution: 327168[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 118671 | 258035 630957 | 86011 50460 3384068 67.1 | 1.861 % | c | 118772 | 258035 630957 | 94612 50561 3384947 66.9 | 1.862 % | c | 118922 | 258035 630957 | 104073 50711 3385943 66.8 | 1.862 % | c | 119147 | 258035 630957 | 114480 50936 3393108 66.6 | 1.862 % | c | 119485 | 257975 630822 | 125928 51270 3408370 66.5 | 1.880 % | c | 119991 | 257973 630818 | 138521 51775 3435578 66.4 | 1.882 % | c | 120751 | 257967 630806 | 152373 52534 3481224 66.3 | 1.885 % | c ============================================================================== c [1mFound solution: 327087[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 121845 | 257978 630834 | 85992 53628 3589608 66.9 | 1.885 % | c | 121945 | 257978 630834 | 94591 53728 3590157 66.8 | 1.886 % | c | 122095 | 257978 630834 | 104050 53878 3590947 66.6 | 1.886 % | c | 122320 | 257968 630814 | 114455 54102 3595243 66.5 | 1.891 % | c | 122657 | 257968 630814 | 125900 54439 3621169 66.5 | 1.891 % | c | 123163 | 257968 630814 | 138490 54945 3657376 66.6 | 1.891 % | c | 123922 | 257962 630802 | 152340 55702 3697323 66.4 | 1.895 % | c ============================================================================== c [1mFound solution: 326761[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 124101 | 257978 630840 | 85992 55881 3725280 66.7 | 1.895 % | c | 124201 | 257973 630830 | 94591 55980 3736888 66.8 | 1.898 % | c | 124353 | 257973 630830 | 104050 56132 3744535 66.7 | 1.898 % | c ============================================================================== c [1mFound solution: 325755[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 124528 | 257984 630856 | 85994 56307 3761684 66.8 | 1.898 % | c | 124628 | 257984 630856 | 94593 56407 3762535 66.7 | 1.899 % | c | 124780 | 257984 630856 | 104052 56559 3765066 66.6 | 1.899 % | c | 125005 | 257984 630856 | 114458 56784 3767067 66.3 | 1.899 % | c | 125342 | 257976 630840 | 125903 57120 3790584 66.4 | 1.903 % | c ============================================================================== c [1mFound solution: 324296[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 125572 | 257985 630861 | 85995 57350 3807964 66.4 | 1.903 % | c | 125675 | 257985 630861 | 94594 57453 3816308 66.4 | 1.904 % | c | 125827 | 257985 630861 | 104053 57605 3827887 66.5 | 1.904 % | c | 126052 | 257985 630861 | 114459 57830 3843328 66.5 | 1.904 % | c | 126389 | 257985 630861 | 125905 58167 3869622 66.5 | 1.904 % | c | 126897 | 257985 630861 | 138495 58675 3926248 66.9 | 1.904 % | c | 127657 | 257985 630861 | 152345 59435 3970340 66.8 | 1.904 % | c | 128797 | 257985 630861 | 167579 60575 4091789 67.5 | 1.904 % | c ============================================================================== c [1mFound solution: 324294[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 129958 | 257989 630870 | 85996 61736 4150369 67.2 | 1.904 % | c | 130058 | 257989 630870 | 94595 61836 4156458 67.2 | 1.905 % | c | 130208 | 257989 630870 | 104055 61986 4157553 67.1 | 1.905 % | c | 130435 | 257989 630870 | 114460 62213 4163857 66.9 | 1.905 % | c | 130773 | 257989 630870 | 125906 62551 4212703 67.3 | 1.905 % | c | 131280 | 257989 630870 | 138497 63058 4277068 67.8 | 1.905 % | c ============================================================================== c [1mFound solution: 324261[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 131425 | 258003 630905 | 86001 63203 4296758 68.0 | 1.905 % | c | 131527 | 258003 630905 | 94601 63305 4297414 67.9 | 1.906 % | c | 131678 | 258003 630905 | 104061 63456 4298367 67.7 | 1.906 % | c | 131903 | 258003 630905 | 114467 63681 4317691 67.8 | 1.906 % | c | 132241 | 258003 630905 | 125914 64019 4334770 67.7 | 1.906 % | c | 132748 | 258003 630905 | 138505 64526 4366368 67.7 | 1.906 % | c ============================================================================== c [1mFound solution: 323811[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 133502 | 258012 630926 | 86004 65280 4440378 68.0 | 1.906 % | c | 133603 | 258012 630926 | 94604 65381 4449184 68.1 | 1.907 % | c | 133753 | 258012 630926 | 104064 65531 4485658 68.5 | 1.907 % | c | 133979 | 258012 630926 | 114471 65757 4494120 68.3 | 1.907 % | c | 134316 | 258012 630926 | 125918 66094 4535646 68.6 | 1.907 % | c ============================================================================== c [1mFound solution: 323792[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 134432 | 258026 630960 | 86008 66210 4546111 68.7 | 1.907 % | c | 134532 | 258026 630960 | 94608 66310 4548959 68.6 | 1.908 % | c | 134683 | 258018 630942 | 104069 66460 4550008 68.5 | 1.910 % | c | 134908 | 258018 630942 | 114476 66685 4553484 68.3 | 1.910 % | c | 135245 | 258018 630942 | 125924 67022 4569647 68.2 | 1.910 % | c | 135751 | 258018 630942 | 138516 67528 4644702 68.8 | 1.910 % | c ============================================================================== c [1mFound solution: 274665[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 136125 | 258042 631003 | 86014 67902 4677304 68.9 | 1.910 % | c | 136225 | 257923 630734 | 94615 67999 4677961 68.8 | 1.947 % | c | 136375 | 257905 630693 | 104076 68147 4678723 68.7 | 1.953 % | c | 136600 | 257883 630643 | 114484 68367 4683640 68.5 | 1.959 % | c ============================================================================== c [1mFound solution: 265977[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 136819 | 257890 630660 | 85963 68586 4707183 68.6 | 1.959 % | c | 136919 | 257890 630660 | 94559 68686 4708971 68.6 | 1.960 % | c ============================================================================== c [1mFound solution: 265974[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 137059 | 257897 630678 | 85965 68826 4713599 68.5 | 1.960 % | c | 137159 | 257880 630640 | 94561 68923 4714256 68.4 | 1.969 % | c | 137309 | 257880 630640 | 104017 69073 4717909 68.3 | 1.969 % | c ============================================================================== c [1mFound solution: 265005[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 137468 | 257889 630662 | 85963 69232 4721996 68.2 | 1.969 % | c | 137568 | 257889 630662 | 94559 69332 4726681 68.2 | 1.970 % | c ============================================================================== c [1mFound solution: 265000[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 137629 | 257899 630690 | 85966 69393 4732215 68.2 | 1.970 % | c ============================================================================== c [1mFound solution: 264988[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 137670 | 257909 630715 | 85969 69434 4733739 68.2 | 1.970 % | c | 137771 | 257909 630715 | 94565 69535 4738675 68.1 | 1.972 % | c | 137921 | 257909 630715 | 104022 69685 4740505 68.0 | 1.972 % | c | 138147 | 257797 630461 | 114424 69843 4750759 68.0 | 2.007 % | c ============================================================================== c [1mFound solution: 264870[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 138445 | 257806 630483 | 85935 70141 4770299 68.0 | 2.007 % | c | 138545 | 257806 630483 | 94528 70241 4773243 68.0 | 2.008 % | c | 138696 | 257205 629099 | 103981 70359 4777112 67.9 | 2.213 % | c ============================================================================== c [1mFound solution: 264835[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 138822 | 257218 629133 | 85739 70485 4782946 67.9 | 2.213 % | c | 138922 | 257218 629133 | 94312 70585 4788353 67.8 | 2.214 % | c ============================================================================== c [1mFound solution: 264600[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 138951 | 257228 629157 | 85742 70614 4793705 67.9 | 2.214 % | c ============================================================================== c [1mFound solution: 264599[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 139048 | 257240 629186 | 85746 70711 4799831 67.9 | 2.214 % | c | 139149 | 257240 629186 | 94320 70812 4804449 67.8 | 2.216 % | c ============================================================================== c [1mFound solution: 264591[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 139283 | 257252 629215 | 85750 70946 4812382 67.8 | 2.216 % | c | 139384 | 257252 629215 | 94325 71047 4812990 67.7 | 2.217 % | c | 139534 | 257244 629197 | 103757 71196 4814407 67.6 | 2.219 % | c | 139759 | 257244 629197 | 114133 71421 4834542 67.7 | 2.219 % | c ============================================================================== c [1mFound solution: 264585[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 140022 | 256769 628110 | 85589 71638 4896753 68.4 | 2.219 % | c | 140122 | 256769 628110 | 94147 71738 4899538 68.3 | 2.380 % | c | 140272 | 256769 628110 | 103562 71888 4931442 68.6 | 2.380 % | c | 140497 | 256769 628110 | 113918 72113 4939066 68.5 | 2.380 % | c ============================================================================== c [1mFound solution: 264519[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 140666 | 256776 628127 | 85592 72282 4956908 68.6 | 2.380 % | c ============================================================================== c [1mFound solution: 264500[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 140759 | 256786 628152 | 85595 72375 4962193 68.6 | 2.380 % | c | 140859 | 256786 628152 | 94154 72475 4963196 68.5 | 2.382 % | c | 141010 | 256732 628030 | 103569 72615 4971024 68.5 | 2.398 % | c ============================================================================== c [1mFound solution: 264499[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 141130 | 256744 628062 | 85581 72735 4985177 68.5 | 2.398 % | c | 141231 | 256678 627911 | 94139 72827 4985677 68.5 | 2.419 % | c | 141381 | 256416 627313 | 103553 72951 4988588 68.4 | 2.505 % | c | 141607 | 256322 627099 | 113908 73147 4996088 68.3 | 2.534 % | c ============================================================================== c [1mFound solution: 264491[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 141781 | 256332 627126 | 85444 73321 5010594 68.3 | 2.534 % | c | 141883 | 256332 627126 | 93988 73423 5018750 68.4 | 2.535 % | c ============================================================================== c [1mFound solution: 264439[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 141943 | 256342 627151 | 85447 73483 5024276 68.4 | 2.535 % | #### 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.93 0.98 0.93 2/54 30558 Raw data (stat): 30558 (runsolver) R 30557 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543906841 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.001 s] Raw data (loadavg): 0.94 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 7919 0 0 0 979 19 0 0 25 0 1 0 543906841 36589568 7587 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8933 7587 603 41 0 8892 0 vsize: 35732 [startup+20.0014 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 8148 0 0 0 1978 20 0 0 25 0 1 0 543906841 37511168 7816 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9158 7816 603 41 0 9117 0 vsize: 36632 [startup+30.0017 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 8244 0 0 0 2977 20 0 0 25 0 1 0 543906841 37834752 7912 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9237 7912 603 41 0 9196 0 vsize: 36948 [startup+40.0021 s] Raw data (loadavg): 0.96 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 8327 0 0 0 3976 20 0 0 25 0 1 0 543906841 38154240 7995 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9315 7995 603 41 0 9274 0 vsize: 37260 [startup+50.0025 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 8422 0 0 0 4977 21 0 0 25 0 1 0 543906841 38555648 8090 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9413 8090 603 41 0 9372 0 vsize: 37652 [startup+60.0025 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 8575 0 0 0 5976 21 0 0 25 0 1 0 543906841 39264256 8243 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9586 8243 603 41 0 9545 0 vsize: 38344 [startup+70.0033 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 8729 0 0 0 6976 22 0 0 25 0 1 0 543906841 39800832 8397 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9717 8397 603 41 0 9676 0 vsize: 38868 [startup+80.0027 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 8882 0 0 0 7975 22 0 0 25 0 1 0 543906841 40476672 8550 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9882 8550 603 41 0 9841 0 vsize: 39528 [startup+90.0027 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 8961 0 0 0 8975 22 0 0 25 0 1 0 543906841 40747008 8629 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9948 8629 603 41 0 9907 0 vsize: 39792 [startup+100.002 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9097 0 0 0 9975 23 0 0 25 0 1 0 543906841 41287680 8765 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10080 8765 603 41 0 10039 0 vsize: 40320 [startup+110.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9193 0 0 0 10975 23 0 0 25 0 1 0 543906841 41807872 8861 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10207 8861 603 41 0 10166 0 vsize: 40828 [startup+120.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9244 0 0 0 11975 23 0 0 25 0 1 0 543906841 42057728 8912 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10268 8912 603 41 0 10227 0 vsize: 41072 [startup+130.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9290 0 0 0 12974 24 0 0 25 0 1 0 543906841 42192896 8958 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10301 8958 603 41 0 10260 0 vsize: 41204 [startup+140.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9372 0 0 0 13974 24 0 0 25 0 1 0 543906841 42598400 9040 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10400 9040 603 41 0 10359 0 vsize: 41600 [startup+150.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9464 0 0 0 14974 24 0 0 25 0 1 0 543906841 42864640 9132 4294967295 134512640 134672761 3221224544 3221223744 134557892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10465 9132 603 41 0 10424 0 vsize: 41860 [startup+160.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9561 0 0 0 15974 25 0 0 25 0 1 0 543906841 43270144 9229 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10564 9229 603 41 0 10523 0 vsize: 42256 [startup+170.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9710 0 0 0 16973 26 0 0 25 0 1 0 543906841 43941888 9378 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10728 9378 603 41 0 10687 0 vsize: 42912 [startup+180.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9771 0 0 0 17973 26 0 0 25 0 1 0 543906841 44077056 9439 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10761 9439 603 41 0 10720 0 vsize: 43044 [startup+190.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9825 0 0 0 18973 26 0 0 25 0 1 0 543906841 44343296 9493 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10826 9493 603 41 0 10785 0 vsize: 43304 [startup+200.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 9922 0 0 0 19973 26 0 0 25 0 1 0 543906841 44744704 9590 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10924 9590 603 41 0 10883 0 vsize: 43696 [startup+210.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10017 0 0 0 20972 27 0 0 25 0 1 0 543906841 45142016 9685 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11021 9685 603 41 0 10980 0 vsize: 44084 [startup+220.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10083 0 0 0 21972 27 0 0 25 0 1 0 543906841 45375488 9751 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11078 9751 603 41 0 11037 0 vsize: 44312 [startup+230.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10159 0 0 0 22972 28 0 0 25 0 1 0 543906841 45641728 9827 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11143 9827 603 41 0 11102 0 vsize: 44572 [startup+240.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10226 0 0 0 23972 28 0 0 25 0 1 0 543906841 45912064 9894 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11209 9894 603 41 0 11168 0 vsize: 44836 [startup+250.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10297 0 0 0 24971 29 0 0 25 0 1 0 543906841 46174208 9965 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11273 9965 603 41 0 11232 0 vsize: 45092 [startup+260.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10380 0 0 0 25971 29 0 0 25 0 1 0 543906841 46575616 10048 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11371 10048 603 41 0 11330 0 vsize: 45484 [startup+270.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10457 0 0 0 26971 30 0 0 25 0 1 0 543906841 46841856 10125 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11436 10125 603 41 0 11395 0 vsize: 45744 [startup+280.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10494 0 0 0 27971 30 0 0 25 0 1 0 543906841 46977024 10162 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11469 10162 603 41 0 11428 0 vsize: 45876 [startup+290.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10579 0 0 0 28971 30 0 0 25 0 1 0 543906841 47378432 10247 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11567 10247 603 41 0 11526 0 vsize: 46268 [startup+300.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10679 0 0 0 29971 30 0 0 25 0 1 0 543906841 47783936 10347 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11666 10347 603 41 0 11625 0 vsize: 46664 [startup+310.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10762 0 0 0 30971 30 0 0 25 0 1 0 543906841 48041984 10430 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11729 10430 603 41 0 11688 0 vsize: 46916 [startup+320.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10863 0 0 0 31971 31 0 0 25 0 1 0 543906841 48570368 10531 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11858 10531 603 41 0 11817 0 vsize: 47432 [startup+330.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 10951 0 0 0 32971 31 0 0 25 0 1 0 543906841 48836608 10619 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11923 10619 603 41 0 11882 0 vsize: 47692 [startup+340.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11022 0 0 0 33971 31 0 0 25 0 1 0 543906841 49106944 10690 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11989 10690 603 41 0 11948 0 vsize: 47956 [startup+350.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11085 0 0 0 34970 32 0 0 25 0 1 0 543906841 49635328 10753 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12118 10753 603 41 0 12077 0 vsize: 48472 [startup+360.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11131 0 0 0 35970 32 0 0 25 0 1 0 543906841 49893376 10799 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12181 10799 603 41 0 12140 0 vsize: 48724 [startup+370.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11187 0 0 0 36970 32 0 0 25 0 1 0 543906841 50024448 10855 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12213 10855 603 41 0 12172 0 vsize: 48852 [startup+380.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11232 0 0 0 37970 33 0 0 25 0 1 0 543906841 50286592 10900 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12277 10900 603 41 0 12236 0 vsize: 49108 [startup+390.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11365 0 0 0 38970 33 0 0 25 0 1 0 543906841 50827264 11033 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12409 11033 603 41 0 12368 0 vsize: 49636 [startup+400.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11534 0 0 0 39970 33 0 0 25 0 1 0 543906841 51494912 11202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12572 11202 603 41 0 12531 0 vsize: 50288 [startup+410.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11574 0 0 0 40970 33 0 0 25 0 1 0 543906841 51625984 11242 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12604 11242 603 41 0 12563 0 vsize: 50416 [startup+420.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11640 0 0 0 41970 34 0 0 25 0 1 0 543906841 51888128 11308 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12668 11308 603 41 0 12627 0 vsize: 50672 [startup+430.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11702 0 0 0 42970 34 0 0 25 0 1 0 543906841 52150272 11370 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12732 11370 603 41 0 12691 0 vsize: 50928 [startup+440.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11758 0 0 0 43970 34 0 0 25 0 1 0 543906841 52359168 11426 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12783 11426 603 41 0 12742 0 vsize: 51132 [startup+450.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11821 0 0 0 44970 34 0 0 25 0 1 0 543906841 52621312 11489 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12847 11489 603 41 0 12806 0 vsize: 51388 [startup+460.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 11936 0 0 0 45970 34 0 0 25 0 1 0 543906841 53153792 11604 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12977 11604 603 41 0 12936 0 vsize: 51908 [startup+470.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12008 0 0 0 46970 35 0 0 25 0 1 0 543906841 53411840 11676 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13040 11676 603 41 0 12999 0 vsize: 52160 [startup+480.009 s] Raw data (loadavg): 1.15 1.02 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12077 0 0 0 47970 35 0 0 25 0 1 0 543906841 53673984 11745 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13104 11745 603 41 0 13063 0 vsize: 52416 [startup+490.009 s] Raw data (loadavg): 1.12 1.02 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12177 0 0 0 48970 35 0 0 25 0 1 0 543906841 54071296 11845 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13201 11845 603 41 0 13160 0 vsize: 52804 [startup+500.009 s] Raw data (loadavg): 1.10 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12275 0 0 0 49970 35 0 0 25 0 1 0 543906841 54472704 11943 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13299 11943 603 41 0 13258 0 vsize: 53196 [startup+510.009 s] Raw data (loadavg): 1.09 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12347 0 0 0 50969 36 0 0 25 0 1 0 543906841 54738944 12015 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13364 12015 603 41 0 13323 0 vsize: 53456 [startup+520.009 s] Raw data (loadavg): 1.07 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12440 0 0 0 51969 36 0 0 25 0 1 0 543906841 55140352 12108 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13462 12108 603 41 0 13421 0 vsize: 53848 [startup+530.009 s] Raw data (loadavg): 1.06 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12537 0 0 0 52969 37 0 0 25 0 1 0 543906841 55525376 12205 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13556 12205 603 41 0 13515 0 vsize: 54224 [startup+540.009 s] Raw data (loadavg): 1.05 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12614 0 0 0 53969 37 0 0 25 0 1 0 543906841 55910400 12282 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13650 12282 603 41 0 13609 0 vsize: 54600 [startup+550.009 s] Raw data (loadavg): 1.04 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12692 0 0 0 54969 37 0 0 25 0 1 0 543906841 56164352 12360 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13712 12360 603 41 0 13671 0 vsize: 54848 [startup+560.009 s] Raw data (loadavg): 1.04 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12774 0 0 0 55969 37 0 0 25 0 1 0 543906841 56553472 12442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13807 12442 603 41 0 13766 0 vsize: 55228 [startup+570.01 s] Raw data (loadavg): 1.03 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12843 0 0 0 56969 38 0 0 25 0 1 0 543906841 56811520 12511 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13870 12511 603 41 0 13829 0 vsize: 55480 [startup+580.01 s] Raw data (loadavg): 1.03 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12939 0 0 0 57968 38 0 0 25 0 1 0 543906841 57208832 12607 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13967 12607 603 41 0 13926 0 vsize: 55868 [startup+590.01 s] Raw data (loadavg): 1.02 1.01 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 12998 0 0 0 58968 39 0 0 25 0 1 0 543906841 57475072 12666 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14032 12666 603 41 0 13991 0 vsize: 56128 [startup+600.01 s] Raw data (loadavg): 1.02 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13064 0 0 0 59968 39 0 0 25 0 1 0 543906841 57741312 12732 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14097 12732 603 41 0 14056 0 vsize: 56388 [startup+610.011 s] Raw data (loadavg): 1.01 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13127 0 0 0 60968 39 0 0 25 0 1 0 543906841 58003456 12795 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14161 12795 603 41 0 14120 0 vsize: 56644 [startup+620.01 s] Raw data (loadavg): 1.01 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13213 0 0 0 61968 40 0 0 25 0 1 0 543906841 58273792 12881 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14227 12881 603 41 0 14186 0 vsize: 56908 [startup+630.01 s] Raw data (loadavg): 1.01 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13301 0 0 0 62967 40 0 0 25 0 1 0 543906841 58662912 12969 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14322 12969 603 41 0 14281 0 vsize: 57288 [startup+640.012 s] Raw data (loadavg): 1.01 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13385 0 0 0 63967 41 0 0 25 0 1 0 543906841 59052032 13053 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14417 13053 603 41 0 14376 0 vsize: 57668 [startup+650.012 s] Raw data (loadavg): 1.01 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13491 0 0 0 64967 41 0 0 25 0 1 0 543906841 59445248 13159 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14513 13159 603 41 0 14472 0 vsize: 58052 [startup+660.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13583 0 0 0 65967 41 0 0 25 0 1 0 543906841 59826176 13251 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14606 13251 603 41 0 14565 0 vsize: 58424 [startup+670.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 66967 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223728 134558332 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+680.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 67967 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+690.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 68967 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+700.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 69967 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+710.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 70967 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+720.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 71967 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+730.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 72967 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+740.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 73968 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+750.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13636 0 0 0 74968 42 0 0 25 0 1 0 543906841 59961344 13304 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+760.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13637 0 0 0 75968 42 0 0 25 0 1 0 543906841 59961344 13305 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13305 603 41 0 14598 0 vsize: 58556 [startup+770.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 76968 42 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+780.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 77968 42 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+790.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 78968 42 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+800.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 79968 43 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+810.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 80968 43 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+820.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 81968 43 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+830.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 82968 43 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+840.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 83968 43 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+850.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 84968 43 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+860.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13638 0 0 0 85969 43 0 0 25 0 1 0 543906841 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14639 13306 603 41 0 14598 0 vsize: 58556 [startup+870.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13646 0 0 0 86969 43 0 0 25 0 1 0 543906841 60149760 13314 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13314 603 41 0 14644 0 vsize: 58740 [startup+880.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13646 0 0 0 87969 43 0 0 25 0 1 0 543906841 60149760 13314 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13314 603 41 0 14644 0 vsize: 58740 [startup+890.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13646 0 0 0 88969 43 0 0 25 0 1 0 543906841 60149760 13314 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13314 603 41 0 14644 0 vsize: 58740 [startup+900.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13646 0 0 0 89969 44 0 0 25 0 1 0 543906841 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13314 603 41 0 14644 0 vsize: 58740 [startup+910.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13646 0 0 0 90969 44 0 0 25 0 1 0 543906841 60149760 13314 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13314 603 41 0 14644 0 vsize: 58740 [startup+920.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13646 0 0 0 91969 44 0 0 25 0 1 0 543906841 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13314 603 41 0 14644 0 vsize: 58740 [startup+930.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13646 0 0 0 92969 44 0 0 25 0 1 0 543906841 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13314 603 41 0 14644 0 vsize: 58740 [startup+940.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13646 0 0 0 93969 44 0 0 25 0 1 0 543906841 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13314 603 41 0 14644 0 vsize: 58740 [startup+950.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13665 0 0 0 94969 44 0 0 25 0 1 0 543906841 60149760 13333 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13333 603 41 0 14644 0 vsize: 58740 [startup+960.014 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13665 0 0 0 95970 44 0 0 25 0 1 0 543906841 60149760 13333 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13333 603 41 0 14644 0 vsize: 58740 [startup+970.014 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13665 0 0 0 96970 44 0 0 25 0 1 0 543906841 60149760 13333 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14685 13333 603 41 0 14644 0 vsize: 58740 [startup+980.014 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13676 0 0 0 97970 44 0 0 25 0 1 0 543906841 60346368 13344 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13344 603 41 0 14692 0 vsize: 58932 [startup+990.014 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13677 0 0 0 98970 44 0 0 25 0 1 0 543906841 60346368 13345 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13345 603 41 0 14692 0 vsize: 58932 [startup+1000.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13678 0 0 0 99970 44 0 0 25 0 1 0 543906841 60346368 13346 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13346 603 41 0 14692 0 vsize: 58932 [startup+1010.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13679 0 0 0 100970 44 0 0 25 0 1 0 543906841 60346368 13347 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13347 603 41 0 14692 0 vsize: 58932 [startup+1020.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13679 0 0 0 101970 44 0 0 25 0 1 0 543906841 60346368 13347 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13347 603 41 0 14692 0 vsize: 58932 [startup+1030.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13679 0 0 0 102970 44 0 0 25 0 1 0 543906841 60346368 13347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13347 603 41 0 14692 0 vsize: 58932 [startup+1040.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13679 0 0 0 103970 44 0 0 25 0 1 0 543906841 60346368 13347 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13347 603 41 0 14692 0 vsize: 58932 [startup+1050.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13679 0 0 0 104971 44 0 0 25 0 1 0 543906841 60346368 13347 4294967295 134512640 134672761 3221224544 3221223728 134559385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13347 603 41 0 14692 0 vsize: 58932 [startup+1060.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13680 0 0 0 105971 44 0 0 25 0 1 0 543906841 60346368 13348 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13348 603 41 0 14692 0 vsize: 58932 [startup+1070.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13681 0 0 0 106971 44 0 0 25 0 1 0 543906841 60346368 13349 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13349 603 41 0 14692 0 vsize: 58932 [startup+1080.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13682 0 0 0 107971 44 0 0 25 0 1 0 543906841 60346368 13350 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13350 603 41 0 14692 0 vsize: 58932 [startup+1090.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13682 0 0 0 108971 44 0 0 25 0 1 0 543906841 60346368 13350 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13350 603 41 0 14692 0 vsize: 58932 [startup+1100.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13691 0 0 0 109971 45 0 0 25 0 1 0 543906841 60346368 13359 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13359 603 41 0 14692 0 vsize: 58932 [startup+1110.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13691 0 0 0 110972 45 0 0 25 0 1 0 543906841 60346368 13359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13359 603 41 0 14692 0 vsize: 58932 [startup+1120.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13697 0 0 0 111972 45 0 0 25 0 1 0 543906841 60346368 13365 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13365 603 41 0 14692 0 vsize: 58932 [startup+1130.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13697 0 0 0 112972 45 0 0 25 0 1 0 543906841 60346368 13365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13365 603 41 0 14692 0 vsize: 58932 [startup+1140.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13697 0 0 0 113972 45 0 0 25 0 1 0 543906841 60346368 13365 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13365 603 41 0 14692 0 vsize: 58932 [startup+1150.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13703 0 0 0 114972 45 0 0 25 0 1 0 543906841 60346368 13371 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13371 603 41 0 14692 0 vsize: 58932 [startup+1160.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13760 0 0 0 115972 45 0 0 25 0 1 0 543906841 60678144 13428 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14814 13428 603 41 0 14773 0 vsize: 59256 [startup+1170.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13763 0 0 0 116972 45 0 0 25 0 1 0 543906841 60678144 13431 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14814 13431 603 41 0 14773 0 vsize: 59256 [startup+1180.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13879 0 0 0 117971 46 0 0 25 0 1 0 543906841 61173760 13547 4294967295 134512640 134672761 3221224544 3221222384 134597176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14935 13547 603 41 0 14894 0 vsize: 59740 [startup+1190.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13929 0 0 0 118971 46 0 0 25 0 1 0 543906841 61370368 13597 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14983 13597 603 41 0 14942 0 vsize: 59932 [startup+1200.02 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 30558 Raw data (stat): 30558 (minisat+) R 30557 26298 26297 0 -1 0 13969 0 0 0 119971 47 0 0 25 0 1 0 543906841 61476864 13637 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15009 13637 603 41 0 14968 0 vsize: 60036 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 1.00 1.00 0.94 1/54 30558 Raw data (stat): 30558 (minisat+) Z 30557 26298 26297 0 -1 12 13972 0 0 0 119971 49 0 0 25 0 1 0 543906841 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.05 CPU time (s): 1200.22 CPU user time (s): 1199.72 CPU system time (s): 0.498924 CPU usage (%): 100.014 Max. virtual memory (Kb): 60036 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####