Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0282.opb |
MD5SUM | a733e9fa1e4e3ac90baf85249f7c3e9a |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 258411 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 282 |
Biggest coefficient in the objective function | 160646 |
Number of bits for the biggest coefficient in the objective function | 18 |
Sum of the numbers in the objective function | 1302615 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 160646 |
Number of bits of the biggest number in a constraint | 18 |
Biggest sum of numbers in a constraint | 1302615 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.01984 |
Number of variables | 282 |
Total number of constraints | 523 |
Number of constraints which are clauses | 177 |
Number of constraints which are cardinality constraints (but not clauses) | 282 |
Number of constraints which are nor clauses,nor cardinality constraints | 64 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 57 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-05-27 06:47:23 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23290 boxname=wulflinc4 idbench=934 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a733e9fa1e4e3ac90baf85249f7c3e9a /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0282.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0282.opb IDLAUNCH: 23290 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 816500 kB Buffers: 33604 kB Cached: 163980 kB SwapCached: 500 kB Active: 52556 kB Inactive: 147432 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 816248 kB SwapTotal: 2097136 kB SwapFree: 2096004 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5788 kB Slab: 12384 kB Committed_AS: 71792 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-27 07:07:53 (client local time) WITH STATUS 152 IN 1229.86 SECONDS stats: 23290 7 1229.86 152 #### 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 14291 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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.91 0.97 0.91 2/54 14287 Raw data (stat): 14287 (runsolver) R 14286 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795886395 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0011 s] Raw data (loadavg): 0.93 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0024 s] Raw data (loadavg): 0.94 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0031 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0036 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.005 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0058 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0062 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0065 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0074 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14291 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.177 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 14292 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.178 s] Raw data (loadavg): 1.07 0.99 0.91 2/55 14344 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.177 s] Raw data (loadavg): 1.06 0.99 0.91 2/55 14344 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.178 s] Raw data (loadavg): 1.05 0.99 0.91 2/55 14344 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.179 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 14344 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.18 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 14344 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.181 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 14344 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.181 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 14344 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.182 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 14344 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.181 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.182 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.183 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.183 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.183 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.184 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.185 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.184 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.184 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.185 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.185 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.186 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.187 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.187 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.187 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14346 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.19 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.2 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.21 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.21 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.21 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.21 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.22 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.22 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.22 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.22 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.22 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.22 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.22 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.23 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.73 s] Raw data (loadavg): 1.00 0.99 0.91 1/53 14348 Raw data (stat): 14287 (minisat+_script) S 14286 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795886395 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.73 CPU time (s): 1229.86 CPU user time (s): 1229.37 CPU system time (s): 0.483926 CPU usage (%): 100.01 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####