Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.02084 |
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 wulflinc9 THE 2005-04-21 05:11:19 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17133 boxname=wulflinc9 idbench=1318 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a733e9fa1e4e3ac90baf85249f7c3e9a /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-p0282.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-p0282.opb /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-p0282.opb IDLAUNCH: 17133 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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: 474728 kB Buffers: 35700 kB Cached: 501492 kB SwapCached: 8 kB Active: 119812 kB Inactive: 420172 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 474476 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6824 kB Slab: 14244 kB Committed_AS: 63580 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 05:31:21 (client local time) WITH STATUS 10 IN 1200.16 SECONDS stats: 17133 7 1200.16 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 % | #### 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.85 0.97 0.91 2/54 2369 Raw data (stat): 2369 (runsolver) R 2368 30854 30853 0 -1 64 3 0 0 0 0 0 0 0 19 0 1 0 484236674 1052672 98 4294967295 134512640 135381576 3221224432 3221219684 134979581 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 98 215 215 0 42 0 vsize: 1028 [startup+10.0013 s] Raw data (loadavg): 0.87 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 7919 0 0 0 979 19 0 0 25 0 1 0 484236674 36589568 7587 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8933 7587 603 41 0 8892 0 vsize: 35732 [startup+20.0015 s] Raw data (loadavg): 0.89 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 8148 0 0 0 1978 20 0 0 25 0 1 0 484236674 37511168 7816 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9158 7816 603 41 0 9117 0 vsize: 36632 [startup+30.0018 s] Raw data (loadavg): 0.91 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 8247 0 0 0 2978 20 0 0 25 0 1 0 484236674 37834752 7915 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9237 7915 603 41 0 9196 0 vsize: 36948 [startup+40.0027 s] Raw data (loadavg): 0.92 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 8328 0 0 0 3977 22 0 0 25 0 1 0 484236674 38154240 7996 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9315 7996 603 41 0 9274 0 vsize: 37260 [startup+50.0029 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 8423 0 0 0 4976 23 0 0 25 0 1 0 484236674 38555648 8091 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9413 8091 603 41 0 9372 0 vsize: 37652 [startup+60.0041 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 8579 0 0 0 5975 23 0 0 25 0 1 0 484236674 39264256 8247 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9586 8247 603 41 0 9545 0 vsize: 38344 [startup+70.0049 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 8729 0 0 0 6974 24 0 0 25 0 1 0 484236674 39800832 8397 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9717 8397 603 41 0 9676 0 vsize: 38868 [startup+80.0052 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 8897 0 0 0 7973 25 0 0 25 0 1 0 484236674 40476672 8565 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9882 8565 603 41 0 9841 0 vsize: 39528 [startup+90.0064 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 8963 0 0 0 8973 26 0 0 25 0 1 0 484236674 40747008 8631 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9948 8631 603 41 0 9907 0 vsize: 39792 [startup+100.007 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9106 0 0 0 9972 27 0 0 25 0 1 0 484236674 41414656 8774 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10111 8774 603 41 0 10070 0 vsize: 40444 [startup+110.009 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9193 0 0 0 10971 27 0 0 25 0 1 0 484236674 41807872 8861 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10207 8861 603 41 0 10166 0 vsize: 40828 [startup+120.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9256 0 0 0 11971 28 0 0 25 0 1 0 484236674 42057728 8924 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10268 8924 603 41 0 10227 0 vsize: 41072 [startup+130.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9293 0 0 0 12970 29 0 0 25 0 1 0 484236674 42192896 8961 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10301 8961 603 41 0 10260 0 vsize: 41204 [startup+140.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9382 0 0 0 13969 30 0 0 25 0 1 0 484236674 42598400 9050 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10400 9050 603 41 0 10359 0 vsize: 41600 [startup+150.011 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9469 0 0 0 14968 31 0 0 25 0 1 0 484236674 42864640 9137 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10465 9137 603 41 0 10424 0 vsize: 41860 [startup+160.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9565 0 0 0 15968 31 0 0 25 0 1 0 484236674 43270144 9233 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10564 9233 603 41 0 10523 0 vsize: 42256 [startup+170.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9716 0 0 0 16967 32 0 0 25 0 1 0 484236674 43941888 9384 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10728 9384 603 41 0 10687 0 vsize: 42912 [startup+180.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9771 0 0 0 17966 32 0 0 25 0 1 0 484236674 44077056 9439 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10761 9439 603 41 0 10720 0 vsize: 43044 [startup+190.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9825 0 0 0 18966 33 0 0 25 0 1 0 484236674 44343296 9493 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10826 9493 603 41 0 10785 0 vsize: 43304 [startup+200.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 9926 0 0 0 19965 34 0 0 25 0 1 0 484236674 44744704 9594 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10924 9594 603 41 0 10883 0 vsize: 43696 [startup+210.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10020 0 0 0 20965 34 0 0 25 0 1 0 484236674 45142016 9688 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11021 9688 603 41 0 10980 0 vsize: 44084 [startup+220.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10083 0 0 0 21965 35 0 0 25 0 1 0 484236674 45375488 9751 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11078 9751 603 41 0 11037 0 vsize: 44312 [startup+230.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10161 0 0 0 22964 35 0 0 25 0 1 0 484236674 45641728 9829 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11143 9829 603 41 0 11102 0 vsize: 44572 [startup+240.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10228 0 0 0 23963 36 0 0 25 0 1 0 484236674 45912064 9896 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11209 9896 603 41 0 11168 0 vsize: 44836 [startup+250.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10309 0 0 0 24963 37 0 0 25 0 1 0 484236674 46309376 9977 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11306 9977 603 41 0 11265 0 vsize: 45224 [startup+260.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10382 0 0 0 25963 37 0 0 25 0 1 0 484236674 46575616 10050 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11371 10050 603 41 0 11330 0 vsize: 45484 [startup+270.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10459 0 0 0 26962 38 0 0 25 0 1 0 484236674 46841856 10127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11436 10127 603 41 0 11395 0 vsize: 45744 [startup+280.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10494 0 0 0 27962 38 0 0 25 0 1 0 484236674 46977024 10162 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11469 10162 603 41 0 11428 0 vsize: 45876 [startup+290.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10581 0 0 0 28961 39 0 0 25 0 1 0 484236674 47378432 10249 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11567 10249 603 41 0 11526 0 vsize: 46268 [startup+300.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10685 0 0 0 29960 40 0 0 25 0 1 0 484236674 47783936 10353 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11666 10353 603 41 0 11625 0 vsize: 46664 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10768 0 0 0 30960 40 0 0 25 0 1 0 484236674 48177152 10436 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11762 10436 603 41 0 11721 0 vsize: 47048 [startup+320.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10869 0 0 0 31960 40 0 0 25 0 1 0 484236674 48570368 10537 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11858 10537 603 41 0 11817 0 vsize: 47432 [startup+330.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 10953 0 0 0 32959 40 0 0 25 0 1 0 484236674 48836608 10621 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11923 10621 603 41 0 11882 0 vsize: 47692 [startup+340.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11024 0 0 0 33959 41 0 0 25 0 1 0 484236674 49106944 10692 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11989 10692 603 41 0 11948 0 vsize: 47956 [startup+350.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11087 0 0 0 34958 42 0 0 25 0 1 0 484236674 49635328 10755 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12118 10755 603 41 0 12077 0 vsize: 48472 [startup+360.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11132 0 0 0 35958 42 0 0 25 0 1 0 484236674 49893376 10800 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12181 10800 603 41 0 12140 0 vsize: 48724 [startup+370.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11191 0 0 0 36957 43 0 0 25 0 1 0 484236674 50151424 10859 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12244 10859 603 41 0 12203 0 vsize: 48976 [startup+380.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11235 0 0 0 37957 43 0 0 25 0 1 0 484236674 50286592 10903 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12277 10903 603 41 0 12236 0 vsize: 49108 [startup+390.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11367 0 0 0 38956 44 0 0 25 0 1 0 484236674 50827264 11035 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12409 11035 603 41 0 12368 0 vsize: 49636 [startup+400.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11534 0 0 0 39956 45 0 0 25 0 1 0 484236674 51494912 11202 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12572 11202 603 41 0 12531 0 vsize: 50288 [startup+410.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11581 0 0 0 40955 45 0 0 25 0 1 0 484236674 51625984 11249 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12604 11249 603 41 0 12563 0 vsize: 50416 [startup+420.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11646 0 0 0 41955 46 0 0 25 0 1 0 484236674 51888128 11314 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12668 11314 603 41 0 12627 0 vsize: 50672 [startup+430.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11702 0 0 0 42954 47 0 0 25 0 1 0 484236674 52150272 11370 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12732 11370 603 41 0 12691 0 vsize: 50928 [startup+440.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11761 0 0 0 43953 47 0 0 25 0 1 0 484236674 52359168 11429 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12783 11429 603 41 0 12742 0 vsize: 51132 [startup+450.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11825 0 0 0 44953 47 0 0 25 0 1 0 484236674 52621312 11493 4294967295 134512640 134672761 3221224544 3221223808 134562470 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12847 11493 603 41 0 12806 0 vsize: 51388 [startup+460.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 11943 0 0 0 45953 48 0 0 25 0 1 0 484236674 53153792 11611 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12977 11611 603 41 0 12936 0 vsize: 51908 [startup+470.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12011 0 0 0 46952 48 0 0 25 0 1 0 484236674 53411840 11679 4294967295 134512640 134672761 3221224544 3221223712 134561272 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13040 11679 603 41 0 12999 0 vsize: 52160 [startup+480.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12081 0 0 0 47952 49 0 0 25 0 1 0 484236674 53673984 11749 4294967295 134512640 134672761 3221224544 3221223648 134560207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13104 11749 603 41 0 13063 0 vsize: 52416 [startup+490.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12182 0 0 0 48951 49 0 0 25 0 1 0 484236674 54071296 11850 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13201 11850 603 41 0 13160 0 vsize: 52804 [startup+500.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12281 0 0 0 49951 50 0 0 25 0 1 0 484236674 54472704 11949 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13299 11949 603 41 0 13258 0 vsize: 53196 [startup+510.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12352 0 0 0 50951 50 0 0 25 0 1 0 484236674 54738944 12020 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13364 12020 603 41 0 13323 0 vsize: 53456 [startup+520.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12443 0 0 0 51950 51 0 0 25 0 1 0 484236674 55140352 12111 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13462 12111 603 41 0 13421 0 vsize: 53848 [startup+530.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12541 0 0 0 52950 51 0 0 25 0 1 0 484236674 55525376 12209 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13556 12209 603 41 0 13515 0 vsize: 54224 [startup+540.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12619 0 0 0 53949 52 0 0 25 0 1 0 484236674 55910400 12287 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13650 12287 603 41 0 13609 0 vsize: 54600 [startup+550.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12697 0 0 0 54949 53 0 0 25 0 1 0 484236674 56164352 12365 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13712 12365 603 41 0 13671 0 vsize: 54848 [startup+560.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12780 0 0 0 55948 53 0 0 25 0 1 0 484236674 56553472 12448 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13807 12448 603 41 0 13766 0 vsize: 55228 [startup+570.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12849 0 0 0 56948 54 0 0 25 0 1 0 484236674 56811520 12517 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13870 12517 603 41 0 13829 0 vsize: 55480 [startup+580.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12940 0 0 0 57947 54 0 0 25 0 1 0 484236674 57208832 12608 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13967 12608 603 41 0 13926 0 vsize: 55868 [startup+590.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 12998 0 0 0 58947 54 0 0 25 0 1 0 484236674 57475072 12666 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14032 12666 603 41 0 13991 0 vsize: 56128 [startup+600.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13067 0 0 0 59947 55 0 0 25 0 1 0 484236674 57741312 12735 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14097 12735 603 41 0 14056 0 vsize: 56388 [startup+610.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13129 0 0 0 60947 55 0 0 25 0 1 0 484236674 58003456 12797 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14161 12797 603 41 0 14120 0 vsize: 56644 [startup+620.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13217 0 0 0 61947 56 0 0 25 0 1 0 484236674 58273792 12885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14227 12885 603 41 0 14186 0 vsize: 56908 [startup+630.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13305 0 0 0 62946 56 0 0 25 0 1 0 484236674 58662912 12973 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14322 12973 603 41 0 14281 0 vsize: 57288 [startup+640.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13389 0 0 0 63946 57 0 0 25 0 1 0 484236674 59052032 13057 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14417 13057 603 41 0 14376 0 vsize: 57668 [startup+650.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13498 0 0 0 64945 58 0 0 25 0 1 0 484236674 59445248 13166 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14513 13166 603 41 0 14472 0 vsize: 58052 [startup+660.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13589 0 0 0 65944 59 0 0 25 0 1 0 484236674 59826176 13257 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14606 13257 603 41 0 14565 0 vsize: 58424 [startup+670.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 66943 59 0 0 25 0 1 0 484236674 59961344 13304 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+680.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 67943 60 0 0 25 0 1 0 484236674 59961344 13304 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+690.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 68943 60 0 0 25 0 1 0 484236674 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14639 13304 603 41 0 14598 0 vsize: 58556 [startup+700.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 69943 60 0 0 25 0 1 0 484236674 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560871 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.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 70943 60 0 0 25 0 1 0 484236674 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+720.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 71943 60 0 0 25 0 1 0 484236674 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.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 72943 60 0 0 25 0 1 0 484236674 59961344 13304 4294967295 134512640 134672761 3221224544 3221223648 134559925 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.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 73943 60 0 0 25 0 1 0 484236674 59961344 13304 4294967295 134512640 134672761 3221224544 3221223600 134565045 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.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13636 0 0 0 74944 60 0 0 25 0 1 0 484236674 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134561385 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.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13637 0 0 0 75944 60 0 0 25 0 1 0 484236674 59961344 13305 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 76944 60 0 0 25 0 1 0 484236674 59961344 13306 4294967295 134512640 134672761 3221224544 3221223680 134560588 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.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 77944 60 0 0 25 0 1 0 484236674 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134559914 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.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 78944 60 0 0 25 0 1 0 484236674 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 79945 60 0 0 25 0 1 0 484236674 59961344 13306 4294967295 134512640 134672761 3221224544 3221223744 134557822 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.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 80945 60 0 0 25 0 1 0 484236674 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560293 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.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 81945 60 0 0 25 0 1 0 484236674 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134561391 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.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 82945 60 0 0 25 0 1 0 484236674 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+840.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 83945 60 0 0 25 0 1 0 484236674 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 84945 60 0 0 25 0 1 0 484236674 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560235 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.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13638 0 0 0 85945 60 0 0 25 0 1 0 484236674 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+870.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13646 0 0 0 86946 60 0 0 25 0 1 0 484236674 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+880.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13646 0 0 0 87946 60 0 0 25 0 1 0 484236674 60149760 13314 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13646 0 0 0 88946 61 0 0 25 0 1 0 484236674 60149760 13314 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13646 0 0 0 89946 61 0 0 25 0 1 0 484236674 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+910.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13646 0 0 0 90946 61 0 0 25 0 1 0 484236674 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+920.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13646 0 0 0 91946 61 0 0 25 0 1 0 484236674 60149760 13314 4294967295 134512640 134672761 3221224544 3221223680 134565045 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.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13646 0 0 0 92946 61 0 0 25 0 1 0 484236674 60149760 13314 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13646 0 0 0 93947 61 0 0 25 0 1 0 484236674 60149760 13314 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13665 0 0 0 94947 61 0 0 25 0 1 0 484236674 60149760 13333 4294967295 134512640 134672761 3221224544 3221223744 134557895 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.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13665 0 0 0 95947 61 0 0 25 0 1 0 484236674 60149760 13333 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13665 0 0 0 96947 61 0 0 25 0 1 0 484236674 60149760 13333 4294967295 134512640 134672761 3221224544 3221223648 134560370 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.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13676 0 0 0 97947 61 0 0 25 0 1 0 484236674 60346368 13344 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13677 0 0 0 98948 61 0 0 25 0 1 0 484236674 60346368 13345 4294967295 134512640 134672761 3221224544 3221223648 134559847 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.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13678 0 0 0 99948 61 0 0 25 0 1 0 484236674 60346368 13346 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13678 0 0 0 100948 61 0 0 25 0 1 0 484236674 60346368 13346 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13346 603 41 0 14692 0 vsize: 58932 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13679 0 0 0 101948 61 0 0 25 0 1 0 484236674 60346368 13347 4294967295 134512640 134672761 3221224544 3221223648 134559937 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.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13679 0 0 0 102948 61 0 0 25 0 1 0 484236674 60346368 13347 4294967295 134512640 134672761 3221224544 3221223680 134560611 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13679 0 0 0 103948 61 0 0 25 0 1 0 484236674 60346368 13347 4294967295 134512640 134672761 3221224544 3221223688 134560555 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13679 0 0 0 104949 61 0 0 25 0 1 0 484236674 60346368 13347 4294967295 134512640 134672761 3221224544 3221223648 134560218 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13679 0 0 0 105949 61 0 0 25 0 1 0 484236674 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+1070.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13681 0 0 0 106949 61 0 0 25 0 1 0 484236674 60346368 13349 4294967295 134512640 134672761 3221224544 3221223744 134557887 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13682 0 0 0 107949 61 0 0 25 0 1 0 484236674 60346368 13350 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13682 0 0 0 108949 61 0 0 25 0 1 0 484236674 60346368 13350 4294967295 134512640 134672761 3221224544 3221223712 134560885 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13691 0 0 0 109949 61 0 0 25 0 1 0 484236674 60346368 13359 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13691 0 0 0 110949 61 0 0 25 0 1 0 484236674 60346368 13359 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13692 0 0 0 111949 61 0 0 25 0 1 0 484236674 60346368 13360 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13360 603 41 0 14692 0 vsize: 58932 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13697 0 0 0 112950 61 0 0 25 0 1 0 484236674 60346368 13365 4294967295 134512640 134672761 3221224544 3221223680 134560588 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13697 0 0 0 113950 61 0 0 25 0 1 0 484236674 60346368 13365 4294967295 134512640 134672761 3221224544 3221223744 134557885 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.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13698 0 0 0 114950 61 0 0 25 0 1 0 484236674 60346368 13366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14733 13366 603 41 0 14692 0 vsize: 58932 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13717 0 0 0 115950 62 0 0 25 0 1 0 484236674 60416000 13385 4294967295 134512640 134672761 3221224544 3221222664 1075349616 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14750 13385 603 41 0 14709 0 vsize: 59000 [startup+1170.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13760 0 0 0 116950 62 0 0 25 0 1 0 484236674 60678144 13428 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14814 13428 603 41 0 14773 0 vsize: 59256 [startup+1180.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13851 0 0 0 117950 62 0 0 25 0 1 0 484236674 61038592 13519 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14902 13519 603 41 0 14861 0 vsize: 59608 [startup+1190.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13906 0 0 0 118950 62 0 0 25 0 1 0 484236674 61267968 13574 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14958 13574 603 41 0 14917 0 vsize: 59832 [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 2369 Raw data (stat): 2369 (minisat+) R 2368 30854 30853 0 -1 0 13931 0 0 0 119951 62 0 0 25 0 1 0 484236674 61370368 13599 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14983 13599 603 41 0 14942 0 vsize: 59932 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 2369 Raw data (stat): 2369 (minisat+) Z 2368 30854 30853 0 -1 12 13934 0 0 0 119951 64 0 0 25 0 1 0 484236674 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.08 CPU time (s): 1200.16 CPU user time (s): 1199.51 CPU system time (s): 0.648901 CPU usage (%): 100.007 Max. virtual memory (Kb): 59932 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####