Name | normalized-opb/submitted/een/normalized-l152lav.opb |
MD5SUM | 7ef542195551d721d26b015e392d6d4b |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1989 |
Biggest coefficient in the objective function | 268 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 382524 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 1961 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 382524 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.237962 |
Number of variables | 1989 |
Total number of constraints | 193 |
Number of constraints which are clauses | 95 |
Number of constraints which are cardinality constraints (but not clauses) | 97 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 3 |
Maximum length of a constraint | 1989 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-04-14 21:36:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=5223 boxname=wulflinc22 idbench=402 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 7ef542195551d721d26b015e392d6d4b /oldhome/oroussel/tmp/wulflinc22/normalized-l152lav.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc22/normalized-l152lav.opb /oldhome/oroussel/tmp/wulflinc22/normalized-l152lav.opb IDLAUNCH: 5223 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 835412 kB Buffers: 32192 kB Cached: 124208 kB SwapCached: 0 kB Active: 25528 kB Inactive: 133692 kB HighTotal: 131008 kB HighFree: 4984 kB LowTotal: 903652 kB LowFree: 830428 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 34348 kB Committed_AS: 63488 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 21:56:29 (client local time) WITH STATUS 0 IN 1200.24 SECONDS stats: 5223 7 1200.24 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 193 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ========================================================================================== c -- Clauses(.)/Splits(s): ...... c ---[ 191]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 189]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 187]---> Adder-cost: 16 maxlim: 8 bits: 4/4 c ---[ 185]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[ 183]---> Adder-cost: 32 maxlim: 17 bits: 5/5 c ---[ 181]---> Adder-cost: 36 maxlim: 19 bits: 5/5 c ---[ 179]---> Adder-cost: 38 maxlim: 20 bits: 5/5 c ---[ 177]---> Adder-cost: 44 maxlim: 22 bits: 5/5 c ---[ 175]---> Adder-cost: 46 maxlim: 24 bits: 5/5 c ---[ 173]---> Adder-cost: 46 maxlim: 25 bits: 5/5 c ---[ 171]---> Adder-cost: 52 maxlim: 29 bits: 5/5 c ---[ 170]---> Adder-cost: 52 maxlim: 29 bits: 5/5 c ---[ 167]---> Adder-cost: 62 maxlim: 30 bits: 6/5 c ---[ 165]---> Adder-cost: 62 maxlim: 30 bits: 6/5 c ---[ 163]---> Adder-cost: 62 maxlim: 33 bits: 6/6 c ---[ 161]---> Adder-cost: 64 maxlim: 33 bits: 6/6 c ---[ 159]---> Adder-cost: 66 maxlim: 35 bits: 6/6 c ---[ 157]---> Adder-cost: 68 maxlim: 35 bits: 6/6 c ---[ 155]---> Adder-cost: 68 maxlim: 35 bits: 6/6 c ---[ 153]---> Adder-cost: 76 maxlim: 38 bits: 6/6 c ---[ 151]---> Adder-cost: 78 maxlim: 40 bits: 6/6 c ---[ 148]---> Adder-cost: 78 maxlim: 40 bits: 6/6 c ---[ 147]---> Adder-cost: 78 maxlim: 40 bits: 6/6 c ---[ 145]---> Adder-cost: 78 maxlim: 41 bits: 6/6 c ---[ 143]---> Adder-cost: 82 maxlim: 42 bits: 6/6 c ---[ 141]---> Adder-cost: 82 maxlim: 42 bits: 6/6 c ---[ 139]---> Adder-cost: 82 maxlim: 42 bits: 6/6 c ---[ 137]---> Adder-cost: 82 maxlim: 43 bits: 6/6 c ---[ 135]---> Adder-cost: 84 maxlim: 44 bits: 6/6 c ---[ 133]---> Adder-cost: 84 maxlim: 45 bits: 6/6 c ---[ 131]---> Adder-cost: 92 maxlim: 46 bits: 6/6 c ---[ 129]---> Adder-cost: 92 maxlim: 46 bits: 6/6 c ---[ 127]---> Adder-cost: 92 maxlim: 46 bits: 6/6 c ---[ 125]---> Adder-cost: 92 maxlim: 47 bits: 6/6 c ---[ 123]---> Adder-cost: 94 maxlim: 48 bits: 6/6 c ---[ 120]---> Adder-cost: 98 maxlim: 50 bits: 6/6 c ---[ 119]---> Adder-cost: 98 maxlim: 50 bits: 6/6 c ---[ 117]---> Adder-cost: 98 maxlim: 51 bits: 6/6 c ---[ 115]---> Adder-cost: 100 maxlim: 52 bits: 6/6 c ---[ 113]---> Adder-cost: 106 maxlim: 54 bits: 6/6 c ---[ 111]---> Adder-cost: 106 maxlim: 54 bits: 6/6 c ---[ 109]---> Adder-cost: 108 maxlim: 56 bits: 6/6 c ---[ 107]---> Adder-cost: 110 maxlim: 58 bits: 6/6 c ---[ 105]---> Adder-cost: 112 maxlim: 60 bits: 6/6 c ---[ 103]---> Adder-cost: 114 maxlim: 60 bits: 6/6 c ---[ 101]---> Adder-cost: 128 maxlim: 64 bits: 7/7 c ---[ 99]---> Adder-cost: 130 maxlim: 66 bits: 7/7 c ---[ 97]---> Adder-cost: 124 maxlim: 66 bits: 7/7 c ---[ 95]---> Adder-cost: 132 maxlim: 66 bits: 7/7 c ---[ 93]---> Adder-cost: 140 maxlim: 71 bits: 7/7 c ---[ 91]---> Adder-cost: 142 maxlim: 72 bits: 7/7 c ---[ 89]---> Adder-cost: 142 maxlim: 73 bits: 7/7 c ---[ 87]---> Adder-cost: 140 maxlim: 73 bits: 7/7 c ---[ 85]---> Adder-cost: 142 maxlim: 73 bits: 7/7 c ---[ 83]---> Adder-cost: 146 maxlim: 74 bits: 7/7 c ---[ 81]---> Adder-cost: 144 maxlim: 75 bits: 7/7 c ---[ 79]---> Adder-cost: 146 maxlim: 75 bits: 7/7 c ---[ 77]---> Adder-cost: 148 maxlim: 76 bits: 7/7 c ---[ 75]---> Adder-cost: 146 maxlim: 77 bits: 7/7 c ---[ 73]---> Adder-cost: 152 maxlim: 78 bits: 7/7 c ---[ 71]---> Adder-cost: 150 maxlim: 85 bits: 7/7 c ---[ 69]---> Adder-cost: 170 maxlim: 86 bits: 7/7 c ---[ 67]---> Adder-cost: 166 maxlim: 86 bits: 7/7 c ---[ 65]---> Adder-cost: 176 maxlim: 90 bits: 7/7 c ---[ 63]---> Adder-cost: 172 maxlim: 90 bits: 7/7 c ---[ 61]---> Adder-cost: 174 maxlim: 90 bits: 7/7 c ---[ 59]---> Adder-cost: 176 maxlim: 91 bits: 7/7 c ---[ 57]---> Adder-cost: 174 maxlim: 92 bits: 7/7 c ---[ 55]---> Adder-cost: 188 maxlim: 94 bits: 7/7 c ---[ 53]---> Adder-cost: 188 maxlim: 94 bits: 7/7 c ---[ 52]---> Adder-cost: 188 maxlim: 94 bits: 7/7 c ---[ 49]---> Adder-cost: 188 maxlim: 95 bits: 7/7 c ---[ 47]---> Adder-cost: 196 maxlim: 100 bits: 7/7 c ---[ 45]---> Adder-cost: 194 maxlim: 100 bits: 7/7 c ---[ 43]---> Adder-cost: 194 maxlim: 101 bits: 7/7 c ---[ 41]---> Adder-cost: 196 maxlim: 102 bits: 7/7 c ---[ 39]---> Adder-cost: 200 maxlim: 104 bits: 7/7 c ---[ 37]---> Adder-cost: 208 maxlim: 106 bits: 7/7 c ---[ 35]---> Adder-cost: 206 maxlim: 106 bits: 7/7 c ---[ 33]---> Adder-cost: 210 maxlim: 110 bits: 7/7 c ---[ 31]---> Adder-cost: 216 maxlim: 110 bits: 7/7 c ---[ 29]---> Adder-cost: 220 maxlim: 112 bits: 7/7 c ---[ 27]---> Adder-cost: 202 maxlim: 116 bits: 7/7 c ---[ 25]---> Adder-cost: 232 maxlim: 119 bits: 7/7 c ---[ 23]---> Adder-cost: 218 maxlim: 119 bits: 7/7 c ---[ 21]---> Adder-cost: 232 maxlim: 121 bits: 7/7 c ---[ 19]---> Adder-cost: 222 maxlim: 123 bits: 7/7 c ---[ 17]---> Adder-cost: 242 maxlim: 126 bits: 8/7 c ---[ 15]---> Adder-cost: 198 maxlim: 127 bits: 8/7 c ---[ 13]---> Adder-cost: 244 maxlim: 135 bits: 8/8 c ---[ 11]---> Adder-cost: 274 maxlim: 150 bits: 8/8 c ---[ 9]---> Adder-cost: 288 maxlim: 158 bits: 8/8 c ---[ 7]---> Adder-cost: 278 maxlim: 161 bits: 8/8 c ---[ 5]---> Adder-cost: 326 maxlim: 169 bits: 8/8 c ---[ 3]---> Adder-cost: 408 maxlim: 216 bits: 8/8 c ---[ 2]---> Adder-cost: 4746 maxlim: 25152 bits: 15/15 c ---[ 0]---> Adder-cost: 3056 maxlim: 1960 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 140156 499983 | 46718 0 0 nan | 0.000 % | c | 100 | 139678 498313 | 51389 34 107 3.1 | 3.561 % | c | 250 | 138747 495023 | 56528 63 202 3.2 | 4.261 % | c | 475 | 138103 492782 | 62181 205 661 3.2 | 4.747 % | c | 812 | 137503 490680 | 68399 471 1537 3.3 | 5.241 % | c | 1318 | 136721 487978 | 75239 875 3267 3.7 | 5.863 % | c | 2077 | 136012 485507 | 82763 1533 6487 4.2 | 6.396 % | c | 3217 | 135680 484372 | 91040 2629 13166 5.0 | 6.650 % | c | 4926 | 135007 482022 | 100144 4241 24192 5.7 | 7.149 % | c | 7489 | 134188 479222 | 110158 6676 47746 7.2 | 7.753 % | c | 11333 | 133638 477293 | 121174 10451 136051 13.0 | 8.142 % | c | 17103 | 133112 475443 | 133291 15886 457002 28.8 | 8.448 % | c | 25752 | 132884 474663 | 146621 24494 1474111 60.2 | 8.614 % | c | 38730 | 132392 472964 | 161283 37360 3089382 82.7 | 8.912 % | c | 58194 | 131811 470939 | 177411 56361 5712628 101.4 | 9.258 % | c | 87386 | 131067 468318 | 195152 84950 9649496 113.6 | 9.769 % | c | 131176 | 130212 465338 | 214667 127951 15890339 124.2 | 10.316 % | c | 196863 | 127772 456732 | 236134 191708 25155652 131.2 | 11.983 % | #### 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.84 0.92 0.90 2/54 4060 Raw data (stat): 4060 (runsolver) R 4059 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487879567 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0005 s] Raw data (loadavg): 0.86 0.92 0.90 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 2899 0 0 0 992 7 0 0 25 0 1 0 487879567 14270464 2817 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3484 2817 603 41 0 3443 0 vsize: 13936 [startup+20.0007 s] Raw data (loadavg): 0.88 0.92 0.90 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 2939 0 0 0 1991 7 0 0 25 0 1 0 487879567 14426112 2857 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3522 2857 603 41 0 3481 0 vsize: 14088 [startup+30.001 s] Raw data (loadavg): 0.90 0.92 0.90 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 2977 0 0 0 2991 8 0 0 25 0 1 0 487879567 14696448 2895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3588 2895 603 41 0 3547 0 vsize: 14352 [startup+40.0007 s] Raw data (loadavg): 0.92 0.92 0.90 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 3159 0 0 0 3990 9 0 0 25 0 1 0 487879567 15368192 3077 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3077 603 41 0 3711 0 vsize: 15008 [startup+50.0008 s] Raw data (loadavg): 0.93 0.93 0.90 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 3642 0 0 0 4989 11 0 0 25 0 1 0 487879567 17371136 3560 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4241 3560 603 41 0 4200 0 vsize: 16964 [startup+60.0011 s] Raw data (loadavg): 0.94 0.93 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 4290 0 0 0 5986 13 0 0 25 0 1 0 487879567 20058112 4208 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4897 4208 603 41 0 4856 0 vsize: 19588 [startup+70.0008 s] Raw data (loadavg): 0.95 0.93 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 4867 0 0 0 6984 15 0 0 25 0 1 0 487879567 22327296 4785 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5451 4785 603 41 0 5410 0 vsize: 21804 [startup+80.0019 s] Raw data (loadavg): 0.95 0.93 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 5423 0 0 0 7982 18 0 0 25 0 1 0 487879567 24596480 5341 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6005 5341 603 41 0 5964 0 vsize: 24020 [startup+90.0023 s] Raw data (loadavg): 0.96 0.93 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 5972 0 0 0 8980 20 0 0 25 0 1 0 487879567 26996736 5890 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6591 5890 603 41 0 6550 0 vsize: 26364 [startup+100.002 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 6344 0 0 0 9979 21 0 0 25 0 1 0 487879567 28483584 6262 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6954 6262 603 41 0 6913 0 vsize: 27816 [startup+110.003 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 6861 0 0 0 10977 23 0 0 25 0 1 0 487879567 30601216 6779 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7471 6779 603 41 0 7430 0 vsize: 29884 [startup+120.003 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 7306 0 0 0 11976 25 0 0 25 0 1 0 487879567 32477184 7224 4294967295 134512640 134672761 3221224560 3221223748 134556588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7929 7224 603 41 0 7888 0 vsize: 31716 [startup+130.004 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 7712 0 0 0 12974 26 0 0 25 0 1 0 487879567 34086912 7630 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8322 7630 603 41 0 8281 0 vsize: 33288 [startup+140.004 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 8167 0 0 0 13973 28 0 0 25 0 1 0 487879567 35946496 8085 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8776 8085 603 41 0 8735 0 vsize: 35104 [startup+150.004 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 8674 0 0 0 14971 29 0 0 25 0 1 0 487879567 37945344 8592 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9264 8592 603 41 0 9223 0 vsize: 37056 [startup+160.004 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 9042 0 0 0 15970 31 0 0 25 0 1 0 487879567 39563264 8960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9659 8960 603 41 0 9618 0 vsize: 38636 [startup+170.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 9365 0 0 0 16969 32 0 0 25 0 1 0 487879567 40886272 9283 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9982 9283 603 41 0 9941 0 vsize: 39928 [startup+180.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 9805 0 0 0 17968 34 0 0 25 0 1 0 487879567 42610688 9723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10403 9723 603 41 0 10362 0 vsize: 41612 [startup+190.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 10087 0 0 0 18967 34 0 0 25 0 1 0 487879567 43823104 10005 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10699 10005 603 41 0 10658 0 vsize: 42796 [startup+200.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 10378 0 0 0 19967 35 0 0 25 0 1 0 487879567 44888064 10296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10959 10296 603 41 0 10918 0 vsize: 43836 [startup+210.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 10722 0 0 0 20966 36 0 0 25 0 1 0 487879567 46616576 10640 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11381 10640 603 41 0 11340 0 vsize: 45524 [startup+220.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 11037 0 0 0 21965 37 0 0 25 0 1 0 487879567 47828992 10955 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11677 10955 603 41 0 11636 0 vsize: 46708 [startup+230.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 11325 0 0 0 22964 38 0 0 25 0 1 0 487879567 49041408 11243 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11973 11243 603 41 0 11932 0 vsize: 47892 [startup+240.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 11698 0 0 0 23963 39 0 0 25 0 1 0 487879567 50524160 11616 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12335 11616 603 41 0 12294 0 vsize: 49340 [startup+250.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 12022 0 0 0 24963 40 0 0 25 0 1 0 487879567 51859456 11940 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12661 11940 603 41 0 12620 0 vsize: 50644 [startup+260.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 12395 0 0 0 25962 41 0 0 25 0 1 0 487879567 53460992 12313 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13052 12313 603 41 0 13011 0 vsize: 52208 [startup+270.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 12660 0 0 0 26961 42 0 0 25 0 1 0 487879567 54530048 12578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13313 12578 603 41 0 13272 0 vsize: 53252 [startup+280.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 12977 0 0 0 27960 43 0 0 25 0 1 0 487879567 55857152 12895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13637 12895 603 41 0 13596 0 vsize: 54548 [startup+290.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 13266 0 0 0 28960 43 0 0 25 0 1 0 487879567 56926208 13184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13898 13184 603 41 0 13857 0 vsize: 55592 [startup+300.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 13529 0 0 0 29959 44 0 0 25 0 1 0 487879567 57995264 13447 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14159 13447 603 41 0 14118 0 vsize: 56636 [startup+310.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 13748 0 0 0 30958 45 0 0 25 0 1 0 487879567 58933248 13666 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14388 13666 603 41 0 14347 0 vsize: 57552 [startup+320.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14044 0 0 0 31958 45 0 0 25 0 1 0 487879567 60125184 13962 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14679 13962 603 41 0 14638 0 vsize: 58716 [startup+330.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14228 0 0 0 32958 46 0 0 25 0 1 0 487879567 60928000 14146 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14875 14146 603 41 0 14834 0 vsize: 59500 [startup+340.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14443 0 0 0 33957 46 0 0 25 0 1 0 487879567 61734912 14361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15072 14361 603 41 0 15031 0 vsize: 60288 [startup+350.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14707 0 0 0 34957 47 0 0 25 0 1 0 487879567 62808064 14625 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15334 14625 603 41 0 15293 0 vsize: 61336 [startup+360.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14992 0 0 0 35956 48 0 0 25 0 1 0 487879567 64004096 14910 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15626 14910 603 41 0 15585 0 vsize: 62504 [startup+370.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 15197 0 0 0 36955 49 0 0 25 0 1 0 487879567 64802816 15115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15821 15115 603 41 0 15780 0 vsize: 63284 [startup+380.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 15413 0 0 0 37955 49 0 0 25 0 1 0 487879567 65732608 15331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16048 15331 603 41 0 16007 0 vsize: 64192 [startup+390.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 15761 0 0 0 38954 51 0 0 25 0 1 0 487879567 67207168 15679 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16408 15679 603 41 0 16367 0 vsize: 65632 [startup+400.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 16067 0 0 0 39954 51 0 0 25 0 1 0 487879567 68411392 15985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16702 15985 603 41 0 16661 0 vsize: 66808 [startup+410.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 16316 0 0 0 40953 51 0 0 25 0 1 0 487879567 69484544 16234 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16964 16234 603 41 0 16923 0 vsize: 67856 [startup+420.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 16561 0 0 0 41953 52 0 0 25 0 1 0 487879567 70410240 16479 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17190 16479 603 41 0 17149 0 vsize: 68760 [startup+430.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 16695 0 0 0 42952 53 0 0 25 0 1 0 487879567 70942720 16613 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17320 16613 603 41 0 17279 0 vsize: 69280 [startup+440.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17001 0 0 0 43952 53 0 0 25 0 1 0 487879567 72282112 16919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17647 16919 603 41 0 17606 0 vsize: 70588 [startup+450.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17268 0 0 0 44951 54 0 0 25 0 1 0 487879567 73351168 17186 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17908 17186 603 41 0 17867 0 vsize: 71632 [startup+460.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17511 0 0 0 45951 55 0 0 25 0 1 0 487879567 74289152 17429 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18137 17429 603 41 0 18096 0 vsize: 72548 [startup+470.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17750 0 0 0 46951 55 0 0 25 0 1 0 487879567 75210752 17668 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18362 17668 603 41 0 18321 0 vsize: 73448 [startup+480.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17991 0 0 0 47950 56 0 0 25 0 1 0 487879567 76279808 17909 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18623 17909 603 41 0 18582 0 vsize: 74492 [startup+490.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 18264 0 0 0 48949 57 0 0 25 0 1 0 487879567 77340672 18182 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18882 18182 603 41 0 18841 0 vsize: 75528 [startup+500.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 18492 0 0 0 49949 58 0 0 25 0 1 0 487879567 78270464 18410 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19109 18410 603 41 0 19068 0 vsize: 76436 [startup+510.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 18764 0 0 0 50948 59 0 0 25 0 1 0 487879567 79462400 18682 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19400 18682 603 41 0 19359 0 vsize: 77600 [startup+520.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 19048 0 0 0 51947 59 0 0 25 0 1 0 487879567 80531456 18966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19661 18966 603 41 0 19620 0 vsize: 78644 [startup+530.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 19365 0 0 0 52947 60 0 0 25 0 1 0 487879567 81866752 19283 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19987 19283 603 41 0 19946 0 vsize: 79948 [startup+540.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 19608 0 0 0 53946 61 0 0 25 0 1 0 487879567 82800640 19526 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20215 19526 603 41 0 20174 0 vsize: 80860 [startup+550.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 19820 0 0 0 54946 61 0 0 25 0 1 0 487879567 83734528 19738 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20443 19738 603 41 0 20402 0 vsize: 81772 [startup+560.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20084 0 0 0 55945 62 0 0 25 0 1 0 487879567 84807680 20002 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20002 603 41 0 20664 0 vsize: 82820 [startup+570.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20290 0 0 0 56944 63 0 0 25 0 1 0 487879567 85626880 20208 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20905 20208 603 41 0 20864 0 vsize: 83620 [startup+580.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20505 0 0 0 57943 64 0 0 25 0 1 0 487879567 86560768 20423 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21133 20423 603 41 0 21092 0 vsize: 84532 [startup+590.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20655 0 0 0 58943 64 0 0 25 0 1 0 487879567 87748608 20573 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21423 20573 603 41 0 21382 0 vsize: 85692 [startup+600.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20780 0 0 0 59942 65 0 0 25 0 1 0 487879567 88141824 20698 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21519 20698 603 41 0 21478 0 vsize: 86076 [startup+610.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20911 0 0 0 60942 65 0 0 25 0 1 0 487879567 88805376 20829 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21681 20829 603 41 0 21640 0 vsize: 86724 [startup+620.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 21183 0 0 0 61941 66 0 0 25 0 1 0 487879567 89858048 21101 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21938 21101 603 41 0 21897 0 vsize: 87752 [startup+630.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 21684 0 0 0 62941 67 0 0 25 0 1 0 487879567 91865088 21602 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22428 21602 603 41 0 22387 0 vsize: 89712 [startup+640.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22060 0 0 0 63940 68 0 0 25 0 1 0 487879567 93466624 21978 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22819 21978 603 41 0 22778 0 vsize: 91276 [startup+650.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22184 0 0 0 64940 68 0 0 25 0 1 0 487879567 94027776 22102 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22956 22102 603 41 0 22915 0 vsize: 91824 [startup+660.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22335 0 0 0 65939 69 0 0 25 0 1 0 487879567 94564352 22253 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23087 22253 603 41 0 23046 0 vsize: 92348 [startup+670.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22606 0 0 0 66939 70 0 0 25 0 1 0 487879567 95637504 22524 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23349 22524 603 41 0 23308 0 vsize: 93396 [startup+680.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22875 0 0 0 67938 70 0 0 25 0 1 0 487879567 96706560 22793 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23610 22793 603 41 0 23569 0 vsize: 94440 [startup+690.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23068 0 0 0 68938 71 0 0 25 0 1 0 487879567 97513472 22986 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23807 22986 603 41 0 23766 0 vsize: 95228 [startup+700.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23250 0 0 0 69937 72 0 0 25 0 1 0 487879567 98316288 23168 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24003 23168 603 41 0 23962 0 vsize: 96012 [startup+710.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23499 0 0 0 70937 72 0 0 25 0 1 0 487879567 99241984 23417 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24229 23417 603 41 0 24188 0 vsize: 96916 [startup+720.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23689 0 0 0 71937 73 0 0 25 0 1 0 487879567 100036608 23607 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24423 23607 603 41 0 24382 0 vsize: 97692 [startup+730.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23890 0 0 0 72936 73 0 0 25 0 1 0 487879567 100962304 23808 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24649 23808 603 41 0 24608 0 vsize: 98596 [startup+740.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24040 0 0 0 73935 74 0 0 25 0 1 0 487879567 101498880 23958 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24780 23958 603 41 0 24739 0 vsize: 99120 [startup+750.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24231 0 0 0 74935 75 0 0 25 0 1 0 487879567 102293504 24149 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24974 24149 603 41 0 24933 0 vsize: 99896 [startup+760.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24429 0 0 0 75935 76 0 0 25 0 1 0 487879567 103100416 24347 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25171 24347 603 41 0 25130 0 vsize: 100684 [startup+770.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24652 0 0 0 76934 76 0 0 25 0 1 0 487879567 104034304 24570 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25399 24570 603 41 0 25358 0 vsize: 101596 [startup+780.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24831 0 0 0 77934 77 0 0 25 0 1 0 487879567 104742912 24749 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25572 24749 603 41 0 25531 0 vsize: 102288 [startup+790.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24986 0 0 0 78934 77 0 0 25 0 1 0 487879567 105406464 24904 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25734 24904 603 41 0 25693 0 vsize: 102936 [startup+800.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25035 0 0 0 79934 77 0 0 25 0 1 0 487879567 105676800 24953 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25800 24953 603 41 0 25759 0 vsize: 103200 [startup+810.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25312 0 0 0 80933 77 0 0 25 0 1 0 487879567 106733568 25230 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26058 25230 603 41 0 26017 0 vsize: 104232 [startup+820.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25516 0 0 0 81933 78 0 0 25 0 1 0 487879567 107540480 25434 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26255 25434 603 41 0 26214 0 vsize: 105020 [startup+830.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25609 0 0 0 82933 79 0 0 25 0 1 0 487879567 108068864 25527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26384 25527 603 41 0 26343 0 vsize: 105536 [startup+840.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25725 0 0 0 83932 79 0 0 25 0 1 0 487879567 108466176 25643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26481 25643 603 41 0 26440 0 vsize: 105924 [startup+850.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25854 0 0 0 84932 79 0 0 25 0 1 0 487879567 109047808 25772 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26623 25772 603 41 0 26582 0 vsize: 106492 [startup+860.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25995 0 0 0 85932 80 0 0 25 0 1 0 487879567 109576192 25913 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26752 25913 603 41 0 26711 0 vsize: 107008 [startup+870.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26150 0 0 0 86932 80 0 0 25 0 1 0 487879567 110235648 26068 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26913 26068 603 41 0 26872 0 vsize: 107652 [startup+880.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26278 0 0 0 87932 80 0 0 25 0 1 0 487879567 110768128 26196 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27043 26196 603 41 0 27002 0 vsize: 108172 [startup+890.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26461 0 0 0 88932 80 0 0 25 0 1 0 487879567 111587328 26379 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27243 26379 603 41 0 27202 0 vsize: 108972 [startup+900.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26589 0 0 0 89932 80 0 0 25 0 1 0 487879567 112119808 26507 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27373 26507 603 41 0 27332 0 vsize: 109492 [startup+910.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26707 0 0 0 90932 81 0 0 25 0 1 0 487879567 112517120 26625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27470 26625 603 41 0 27429 0 vsize: 109880 [startup+920.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26815 0 0 0 91932 81 0 0 25 0 1 0 487879567 112930816 26733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27571 26733 603 41 0 27530 0 vsize: 110284 [startup+930.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27025 0 0 0 92931 82 0 0 25 0 1 0 487879567 113860608 26943 4294967295 134512640 134672761 3221224560 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27798 26943 603 41 0 27757 0 vsize: 111192 [startup+940.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27180 0 0 0 93931 82 0 0 25 0 1 0 487879567 114515968 27098 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27958 27098 603 41 0 27917 0 vsize: 111832 [startup+950.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27350 0 0 0 94930 83 0 0 25 0 1 0 487879567 115179520 27268 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28120 27268 603 41 0 28079 0 vsize: 112480 [startup+960.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27526 0 0 0 95930 84 0 0 25 0 1 0 487879567 115834880 27444 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28280 27444 603 41 0 28239 0 vsize: 113120 [startup+970.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27697 0 0 0 96930 84 0 0 25 0 1 0 487879567 116490240 27615 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28440 27615 603 41 0 28399 0 vsize: 113760 [startup+980.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27828 0 0 0 97929 85 0 0 25 0 1 0 487879567 117157888 27746 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28603 27746 603 41 0 28562 0 vsize: 114412 [startup+990.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27880 0 0 0 98929 85 0 0 25 0 1 0 487879567 117293056 27798 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28636 27798 603 41 0 28595 0 vsize: 114544 [startup+1000.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27971 0 0 0 99929 85 0 0 25 0 1 0 487879567 117698560 27889 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28735 27889 603 41 0 28694 0 vsize: 114940 [startup+1010.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28066 0 0 0 100929 85 0 0 25 0 1 0 487879567 118099968 27984 4294967295 134512640 134672761 3221224560 3221223732 134556596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28833 27984 603 41 0 28792 0 vsize: 115332 [startup+1020.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28172 0 0 0 101929 86 0 0 25 0 1 0 487879567 118497280 28090 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28930 28090 603 41 0 28889 0 vsize: 115720 [startup+1030.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28271 0 0 0 102929 86 0 0 25 0 1 0 487879567 118898688 28189 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29028 28189 603 41 0 28987 0 vsize: 116112 [startup+1040.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28384 0 0 0 103929 86 0 0 25 0 1 0 487879567 119316480 28302 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29130 28302 603 41 0 29089 0 vsize: 116520 [startup+1050.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28548 0 0 0 104929 86 0 0 25 0 1 0 487879567 119984128 28466 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29293 28466 603 41 0 29252 0 vsize: 117172 [startup+1060.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28704 0 0 0 105928 87 0 0 25 0 1 0 487879567 120684544 28622 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29464 28622 603 41 0 29423 0 vsize: 117856 [startup+1070.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28851 0 0 0 106928 88 0 0 25 0 1 0 487879567 121348096 28769 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29626 28769 603 41 0 29585 0 vsize: 118504 [startup+1080.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28996 0 0 0 107927 89 0 0 25 0 1 0 487879567 121872384 28914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29754 28914 603 41 0 29713 0 vsize: 119016 [startup+1090.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29099 0 0 0 108927 89 0 0 25 0 1 0 487879567 122400768 29017 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29883 29017 603 41 0 29842 0 vsize: 119532 [startup+1100.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29186 0 0 0 109927 89 0 0 25 0 1 0 487879567 122662912 29104 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29947 29104 603 41 0 29906 0 vsize: 119788 [startup+1110.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29313 0 0 0 110927 90 0 0 25 0 1 0 487879567 123195392 29231 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30077 29231 603 41 0 30036 0 vsize: 120308 [startup+1120.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29448 0 0 0 111927 90 0 0 25 0 1 0 487879567 123727872 29366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30207 29366 603 41 0 30166 0 vsize: 120828 [startup+1130.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29589 0 0 0 112927 90 0 0 25 0 1 0 487879567 124297216 29507 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30346 29507 603 41 0 30305 0 vsize: 121384 [startup+1140.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29688 0 0 0 113926 91 0 0 25 0 1 0 487879567 124698624 29606 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30444 29606 603 41 0 30403 0 vsize: 121776 [startup+1150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29822 0 0 0 114926 91 0 0 25 0 1 0 487879567 125231104 29740 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30574 29740 603 41 0 30533 0 vsize: 122296 [startup+1160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30006 0 0 0 115925 92 0 0 25 0 1 0 487879567 126029824 29924 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30769 29924 603 41 0 30728 0 vsize: 123076 [startup+1170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30061 0 0 0 116925 92 0 0 25 0 1 0 487879567 126296064 29979 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30834 29979 603 41 0 30793 0 vsize: 123336 [startup+1180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30113 0 0 0 117925 92 0 0 25 0 1 0 487879567 126427136 30031 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30866 30031 603 41 0 30825 0 vsize: 123464 [startup+1190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30225 0 0 0 118925 93 0 0 25 0 1 0 487879567 126963712 30143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30997 30143 603 41 0 30956 0 vsize: 123988 [startup+1200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4060 Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30378 0 0 0 119925 93 0 0 25 0 1 0 487879567 127500288 30296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31128 30296 603 41 0 31087 0 vsize: 124512 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 4060 Raw data (stat): 4060 (minisat+) Z 4059 26298 26297 0 -1 12 30380 0 0 0 119925 98 0 0 25 0 1 0 487879567 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.07 CPU time (s): 1200.24 CPU user time (s): 1199.25 CPU system time (s): 0.988849 CPU usage (%): 100.015 Max. virtual memory (Kb): 124512 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####