Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod010.opb |
MD5SUM | 4f0cac14ed3568050c2c57bb69fdb664 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 6571 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2655 |
Biggest coefficient in the objective function | 266 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 489211 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 266 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 489211 |
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 | 1175.14 |
Number of variables | 2655 |
Total number of constraints | 2801 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 2800 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 2655 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-04-22 02:19:07 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12043 boxname=wulflinc11 idbench=927 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 4f0cac14ed3568050c2c57bb69fdb664 /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod010.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod010.opb IDLAUNCH: 12043 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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: 331896 kB Buffers: 34928 kB Cached: 645956 kB SwapCached: 0 kB Active: 230804 kB Inactive: 452860 kB HighTotal: 131008 kB HighFree: 33516 kB LowTotal: 903652 kB LowFree: 298380 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6820 kB Slab: 13368 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-22 02:39:10 (client local time) WITH STATUS 0 IN 1200.28 SECONDS stats: 12043 7 1200.28 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 291 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################################################################################################# c -- Clauses(.)/Splits(s): (none) c ---[ 289]---> BDD-cost: 67 c ---[ 287]---> BDD-cost: 113 c ---[ 285]---> BDD-cost: 181 c ---[ 283]---> BDD-cost: 115 c ---[ 281]---> BDD-cost: 69 c ---[ 279]---> BDD-cost: 125 c ---[ 277]---> BDD-cost: 155 c ---[ 275]---> BDD-cost: 87 c ---[ 273]---> BDD-cost: 97 c ---[ 271]---> BDD-cost: 73 c ---[ 269]---> BDD-cost: 119 c ---[ 267]---> BDD-cost: 45 c ---[ 265]---> BDD-cost: 171 c ---[ 263]---> BDD-cost: 111 c ---[ 261]---> BDD-cost: 149 c ---[ 259]---> BDD-cost: 195 c ---[ 257]---> BDD-cost: 131 c ---[ 255]---> BDD-cost: 123 c ---[ 253]---> BDD-cost: 167 c ---[ 251]---> BDD-cost: 101 c ---[ 249]---> BDD-cost: 97 c ---[ 247]---> BDD-cost: 23 c ---[ 245]---> BDD-cost: 135 c ---[ 243]---> BDD-cost: 59 c ---[ 241]---> BDD-cost: 95 c ---[ 239]---> BDD-cost: 59 c ---[ 237]---> BDD-cost: 133 c ---[ 235]---> BDD-cost: 99 c ---[ 233]---> BDD-cost: 179 c ---[ 231]---> BDD-cost: 111 c ---[ 229]---> BDD-cost: 23 c ---[ 227]---> BDD-cost: 89 c ---[ 225]---> BDD-cost: 95 c ---[ 223]---> BDD-cost: 117 c ---[ 221]---> BDD-cost: 23 c ---[ 219]---> BDD-cost: 51 c ---[ 217]---> BDD-cost: 311 c ---[ 215]---> BDD-cost: 259 c ---[ 213]---> BDD-cost: 169 c ---[ 211]---> BDD-cost: 131 c ---[ 209]---> BDD-cost: 155 c ---[ 207]---> BDD-cost: 89 c ---[ 205]---> BDD-cost: 51 c ---[ 203]---> BDD-cost: 165 c ---[ 201]---> BDD-cost: 75 c ---[ 199]---> BDD-cost: 139 c ---[ 197]---> BDD-cost: 67 c ---[ 195]---> BDD-cost: 173 c ---[ 193]---> BDD-cost: 235 c ---[ 191]---> BDD-cost: 185 c ---[ 189]---> BDD-cost: 127 c ---[ 187]---> BDD-cost: 37 c ---[ 185]---> BDD-cost: 37 c ---[ 183]---> BDD-cost: 91 c ---[ 181]---> BDD-cost: 77 c ---[ 179]---> BDD-cost: 29 c ---[ 177]---> BDD-cost: 77 c ---[ 175]---> BDD-cost: 77 c ---[ 173]---> BDD-cost: 101 c ---[ 171]---> BDD-cost: 131 c ---[ 169]---> BDD-cost: 155 c ---[ 167]---> BDD-cost: 177 c ---[ 165]---> BDD-cost: 143 c ---[ 163]---> BDD-cost: 93 c ---[ 161]---> BDD-cost: 79 c ---[ 159]---> BDD-cost: 53 c ---[ 157]---> BDD-cost: 71 c ---[ 155]---> BDD-cost: 127 c ---[ 153]---> BDD-cost: 127 c ---[ 151]---> BDD-cost: 67 c ---[ 149]---> BDD-cost: 83 c ---[ 147]---> BDD-cost: 47 c ---[ 145]---> BDD-cost: 63 c ---[ 143]---> BDD-cost: 121 c ---[ 141]---> BDD-cost: 155 c ---[ 139]---> BDD-cost: 87 c ---[ 137]---> BDD-cost: 91 c ---[ 135]---> BDD-cost: 47 c ---[ 133]---> BDD-cost: 67 c ---[ 131]---> BDD-cost: 33 c ---[ 129]---> BDD-cost: 91 c ---[ 127]---> BDD-cost: 69 c ---[ 125]---> BDD-cost: 5 c ---[ 123]---> BDD-cost: 47 c ---[ 121]---> BDD-cost: 45 c ---[ 119]---> BDD-cost: 37 c ---[ 117]---> BDD-cost: 117 c ---[ 115]---> BDD-cost: 97 c ---[ 113]---> BDD-cost: 77 c ---[ 111]---> BDD-cost: 97 c ---[ 109]---> BDD-cost: 137 c ---[ 107]---> BDD-cost: 125 c ---[ 105]---> BDD-cost: 79 c ---[ 103]---> BDD-cost: 133 c ---[ 101]---> BDD-cost: 153 c ---[ 99]---> BDD-cost: 139 c ---[ 97]---> BDD-cost: 125 c ---[ 95]---> BDD-cost: 5 c ---[ 93]---> BDD-cost: 73 c ---[ 91]---> BDD-cost: 157 c ---[ 89]---> BDD-cost: 127 c ---[ 87]---> BDD-cost: 199 c ---[ 85]---> BDD-cost: 121 c ---[ 83]---> BDD-cost: 107 c ---[ 81]---> BDD-cost: 169 c ---[ 79]---> BDD-cost: 113 c ---[ 77]---> BDD-cost: 103 c ---[ 75]---> BDD-cost: 75 c ---[ 73]---> BDD-cost: 97 c ---[ 71]---> BDD-cost: 151 c ---[ 69]---> BDD-cost: 199 c ---[ 67]---> BDD-cost: 109 c ---[ 65]---> BDD-cost: 131 c ---[ 63]---> BDD-cost: 113 c ---[ 61]---> BDD-cost: 173 c ---[ 59]---> BDD-cost: 119 c ---[ 57]---> BDD-cost: 173 c ---[ 55]---> BDD-cost: 119 c ---[ 53]---> BDD-cost: 71 c ---[ 51]---> BDD-cost: 179 c ---[ 49]---> BDD-cost: 241 c ---[ 47]---> BDD-cost: 201 c ---[ 45]---> BDD-cost: 173 c ---[ 43]---> BDD-cost: 147 c ---[ 41]---> BDD-cost: 157 c ---[ 39]---> BDD-cost: 201 c ---[ 37]---> BDD-cost: 129 c ---[ 35]---> BDD-cost: 117 c ---[ 33]---> BDD-cost: 177 c ---[ 31]---> BDD-cost: 123 c ---[ 29]---> BDD-cost: 131 c ---[ 27]---> BDD-cost: 115 c ---[ 25]---> BDD-cost: 51 c ---[ 23]---> BDD-cost: 123 c ---[ 21]---> BDD-cost: 55 c ---[ 19]---> BDD-cost: 5 c ---[ 17]---> BDD-cost: 99 c ---[ 15]---> BDD-cost: 85 c ---[ 13]---> BDD-cost: 109 c ---[ 11]---> BDD-cost: 153 c ---[ 9]---> BDD-cost: 201 c ---[ 7]---> BDD-cost: 133 c ---[ 5]---> BDD-cost: 121 c ---[ 3]---> BDD-cost: 171 c ---[ 1]---> Adder-cost: 5294 maxlim: 2609 bits: 12/12 c ---[ 0]---> BDD-cost: 751 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 79291 242194 | 26430 0 0 nan | 0.000 % | c | 101 | 79216 241933 | 29073 93 735 7.9 | 0.735 % | c | 253 | 79216 241933 | 31980 245 2664 10.9 | 0.735 % | c | 478 | 79216 241933 | 35178 470 26790 57.0 | 0.735 % | c | 816 | 79216 241933 | 38696 808 31842 39.4 | 0.735 % | c | 1323 | 79216 241933 | 42565 1315 62134 47.3 | 0.735 % | c | 2082 | 79216 241933 | 46822 2074 107560 51.9 | 0.735 % | c | 3222 | 79188 241847 | 51504 3207 277140 86.4 | 0.751 % | c | 4930 | 79188 241847 | 56655 4915 483903 98.5 | 0.751 % | c | 7493 | 79188 241847 | 62320 7478 739580 98.9 | 0.751 % | c | 11337 | 79188 241847 | 68552 11322 1362239 120.3 | 0.751 % | c | 17103 | 79164 241769 | 75407 17085 2978250 174.3 | 0.767 % | c | 25752 | 79164 241769 | 82948 25734 6444146 250.4 | 0.767 % | c | 38727 | 79164 241769 | 91243 38709 10596182 273.7 | 0.767 % | c | 58188 | 79145 241708 | 100367 58167 16215504 278.8 | 0.779 % | c | 87383 | 79101 241554 | 110404 87356 23978747 274.5 | 0.807 % | c | 131172 | 79079 241468 | 121445 35237 6368599 180.7 | 0.823 % | c | 196857 | 78549 239688 | 133589 100806 30304920 300.6 | 1.134 % | #### 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.92 0.95 0.91 2/54 16224 Raw data (stat): 16224 (runsolver) R 16223 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491841918 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0008 s] Raw data (loadavg): 0.93 0.95 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 5367 0 0 0 984 14 0 0 25 0 1 0 491841918 22274048 4698 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5438 4698 603 41 0 5397 0 vsize: 21752 [startup+20.001 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 5909 0 0 0 1982 15 0 0 25 0 1 0 491841918 24596480 5240 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6005 5240 603 41 0 5964 0 vsize: 24020 [startup+30.0018 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 6489 0 0 0 2980 17 0 0 25 0 1 0 491841918 26890240 5820 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6565 5820 603 41 0 6524 0 vsize: 26260 [startup+40.0019 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 7296 0 0 0 3978 20 0 0 25 0 1 0 491841918 30257152 6627 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7387 6627 603 41 0 7346 0 vsize: 29548 [startup+50.0013 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 8020 0 0 0 4976 21 0 0 25 0 1 0 491841918 33226752 7351 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8112 7351 603 41 0 8071 0 vsize: 32448 [startup+60.0011 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 8667 0 0 0 5975 23 0 0 25 0 1 0 491841918 35872768 7998 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8758 7998 603 41 0 8717 0 vsize: 35032 [startup+70.0012 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 9300 0 0 0 6972 26 0 0 25 0 1 0 491841918 38436864 8631 4294967295 134512640 134672761 3221224624 3221223728 134560252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9384 8631 603 41 0 9343 0 vsize: 37536 [startup+80.0017 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 9922 0 0 0 7971 27 0 0 25 0 1 0 491841918 40992768 9253 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10008 9253 603 41 0 9967 0 vsize: 40032 [startup+90.0015 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 10501 0 0 0 8970 29 0 0 25 0 1 0 491841918 43413504 9832 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10599 9832 603 41 0 10558 0 vsize: 42396 [startup+100.002 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 11053 0 0 0 9967 31 0 0 25 0 1 0 491841918 45703168 10384 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11158 10384 603 41 0 11117 0 vsize: 44632 [startup+110.002 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 11598 0 0 0 10966 32 0 0 25 0 1 0 491841918 47841280 10929 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11680 10929 603 41 0 11639 0 vsize: 46720 [startup+120.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 12225 0 0 0 11964 35 0 0 25 0 1 0 491841918 50397184 11556 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12304 11557 603 41 0 12263 0 vsize: 49216 [startup+130.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 12961 0 0 0 12963 36 0 0 25 0 1 0 491841918 53489664 12292 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13059 12292 603 41 0 13018 0 vsize: 52236 [startup+140.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 13608 0 0 0 13961 38 0 0 25 0 1 0 491841918 56164352 12939 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13712 12939 603 41 0 13671 0 vsize: 54848 [startup+150.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 14296 0 0 0 14960 39 0 0 25 0 1 0 491841918 58859520 13627 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14370 13627 603 41 0 14329 0 vsize: 57480 [startup+160.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 14915 0 0 0 15959 41 0 0 25 0 1 0 491841918 61554688 14246 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15028 14246 603 41 0 14987 0 vsize: 60112 [startup+170.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 15517 0 0 0 16957 42 0 0 25 0 1 0 491841918 63979520 14848 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15620 14848 603 41 0 15579 0 vsize: 62480 [startup+180.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 16133 0 0 0 17956 44 0 0 25 0 1 0 491841918 66535424 15464 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16244 15464 603 41 0 16203 0 vsize: 64976 [startup+190.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 16685 0 0 0 18955 45 0 0 25 0 1 0 491841918 68820992 16016 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16802 16016 603 41 0 16761 0 vsize: 67208 [startup+200.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 17403 0 0 0 19953 47 0 0 25 0 1 0 491841918 71794688 16734 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17528 16734 603 41 0 17487 0 vsize: 70112 [startup+210.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 18177 0 0 0 20951 50 0 0 25 0 1 0 491841918 74899456 17508 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18286 17508 603 41 0 18245 0 vsize: 73144 [startup+220.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 18877 0 0 0 21949 52 0 0 25 0 1 0 491841918 77737984 18208 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18979 18208 603 41 0 18938 0 vsize: 75916 [startup+230.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 19510 0 0 0 22948 53 0 0 25 0 1 0 491841918 80285696 18841 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19601 18841 603 41 0 19560 0 vsize: 78404 [startup+240.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 20156 0 0 0 23946 55 0 0 25 0 1 0 491841918 82984960 19487 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20260 19487 603 41 0 20219 0 vsize: 81040 [startup+250.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 20757 0 0 0 24945 56 0 0 25 0 1 0 491841918 85417984 20088 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20854 20088 603 41 0 20813 0 vsize: 83416 [startup+260.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 21373 0 0 0 25944 58 0 0 25 0 1 0 491841918 87990272 20704 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21482 20704 603 41 0 21441 0 vsize: 85928 [startup+270.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 21828 0 0 0 26942 59 0 0 25 0 1 0 491841918 89874432 21159 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21942 21159 603 41 0 21901 0 vsize: 87768 [startup+280.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 22348 0 0 0 27940 61 0 0 25 0 1 0 491841918 91897856 21679 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22436 21679 603 41 0 22395 0 vsize: 89744 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 22978 0 0 0 28938 63 0 0 25 0 1 0 491841918 94588928 22309 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23093 22309 603 41 0 23052 0 vsize: 92372 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 23589 0 0 0 29937 65 0 0 25 0 1 0 491841918 97001472 22920 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23682 22920 603 41 0 23641 0 vsize: 94728 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 24036 0 0 0 30937 66 0 0 25 0 1 0 491841918 99151872 23367 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24207 23367 603 41 0 24166 0 vsize: 96828 [startup+320.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 24612 0 0 0 31937 67 0 0 25 0 1 0 491841918 101441536 23943 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24766 23943 603 41 0 24725 0 vsize: 99064 [startup+330.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 25055 0 0 0 32937 68 0 0 25 0 1 0 491841918 103333888 24386 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25228 24387 603 41 0 25187 0 vsize: 100912 [startup+340.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 25639 0 0 0 33936 69 0 0 25 0 1 0 491841918 105611264 24970 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25784 24970 603 41 0 25743 0 vsize: 103136 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 26394 0 0 0 34934 71 0 0 25 0 1 0 491841918 108703744 25725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26539 25725 603 41 0 26498 0 vsize: 106156 [startup+360.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 27167 0 0 0 35933 72 0 0 25 0 1 0 491841918 111943680 26498 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27330 26498 603 41 0 27289 0 vsize: 109320 [startup+370.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 27713 0 0 0 36932 74 0 0 25 0 1 0 491841918 114098176 27044 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27856 27044 603 41 0 27815 0 vsize: 111424 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 28098 0 0 0 37931 75 0 0 25 0 1 0 491841918 115712000 27429 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28250 27429 603 41 0 28209 0 vsize: 113000 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 28545 0 0 0 38930 76 0 0 25 0 1 0 491841918 117600256 27876 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28711 27876 603 41 0 28670 0 vsize: 114844 [startup+400.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 28992 0 0 0 39929 77 0 0 25 0 1 0 491841918 119361536 28323 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29141 28323 603 41 0 29100 0 vsize: 116564 [startup+410.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 29504 0 0 0 40929 77 0 0 25 0 1 0 491841918 121393152 28835 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29637 28835 603 41 0 29596 0 vsize: 118548 [startup+420.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 30057 0 0 0 41928 79 0 0 25 0 1 0 491841918 123686912 29388 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30197 29388 603 41 0 30156 0 vsize: 120788 [startup+430.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 30617 0 0 0 42925 81 0 0 25 0 1 0 491841918 125984768 29948 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30758 29948 603 41 0 30717 0 vsize: 123032 [startup+440.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 31330 0 0 0 43922 83 0 0 25 0 1 0 491841918 128913408 30661 4294967295 134512640 134672761 3221224624 3221223728 134559958 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31473 30661 603 41 0 31432 0 vsize: 125892 [startup+450.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 32021 0 0 0 44921 84 0 0 25 0 1 0 491841918 131739648 31352 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32163 31352 603 41 0 32122 0 vsize: 128652 [startup+460.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 32671 0 0 0 45919 87 0 0 25 0 1 0 491841918 134426624 32002 4294967295 134512640 134672761 3221224624 3221223728 134560303 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32819 32002 603 41 0 32778 0 vsize: 131276 [startup+470.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 33259 0 0 0 46918 88 0 0 25 0 1 0 491841918 136720384 32590 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33379 32590 603 41 0 33338 0 vsize: 133516 [startup+480.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 33859 0 0 0 47917 89 0 0 25 0 1 0 491841918 139296768 33190 4294967295 134512640 134672761 3221224624 3221223728 134560198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34008 33190 603 41 0 33967 0 vsize: 136032 [startup+490.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 34445 0 0 0 48915 91 0 0 25 0 1 0 491841918 141619200 33776 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34575 33776 603 41 0 34534 0 vsize: 138300 [startup+500.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 34929 0 0 0 49914 93 0 0 25 0 1 0 491841918 143630336 34260 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35066 34260 603 41 0 35025 0 vsize: 140264 [startup+510.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 35439 0 0 0 50913 94 0 0 25 0 1 0 491841918 145653760 34770 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35560 34770 603 41 0 35519 0 vsize: 142240 [startup+520.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 35883 0 0 0 51912 95 0 0 25 0 1 0 491841918 147542016 35214 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 36021 35214 603 41 0 35980 0 vsize: 144084 [startup+530.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 36420 0 0 0 52911 96 0 0 25 0 1 0 491841918 149700608 35751 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 36548 35751 603 41 0 36507 0 vsize: 146192 [startup+540.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 36943 0 0 0 53909 98 0 0 25 0 1 0 491841918 151859200 36274 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37075 36274 603 41 0 37034 0 vsize: 148300 [startup+550.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 37246 0 0 0 54909 98 0 0 25 0 1 0 491841918 153075712 36577 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37372 36577 603 41 0 37331 0 vsize: 149488 [startup+560.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 37678 0 0 0 55908 99 0 0 25 0 1 0 491841918 154841088 37009 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37803 37009 603 41 0 37762 0 vsize: 151212 [startup+570.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 38137 0 0 0 56907 101 0 0 25 0 1 0 491841918 156733440 37468 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 38265 37468 603 41 0 38224 0 vsize: 153060 [startup+580.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 38693 0 0 0 57906 102 0 0 25 0 1 0 491841918 159027200 38024 4294967295 134512640 134672761 3221224624 3221223728 134559995 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 38825 38024 603 41 0 38784 0 vsize: 155300 [startup+590.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39268 0 0 0 58905 103 0 0 25 0 1 0 491841918 161320960 38599 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39385 38599 603 41 0 39344 0 vsize: 157540 [startup+600.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 59904 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+610.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 60905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+620.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 61905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+630.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 62905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+640.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 63905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+650.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 64905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+660.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 65905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+670.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 66905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+680.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 67905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+690.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 68905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+700.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 69905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559953 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+710.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 70905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+720.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 71905 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+730.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 72906 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+740.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 73906 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+750.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 74906 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+760.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 75906 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+770.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 76906 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+780.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 77907 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+790.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 78907 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+800.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 79907 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559805 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+810.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 80907 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+820.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 81907 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+830.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 82907 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+840.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 83908 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223808 134558918 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+850.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 84908 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+860.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 85908 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+870.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 86908 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+880.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 87909 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560373 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+890.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 88909 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+900.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 89909 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223800 134559059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+910.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 90909 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+920.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 91909 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+930.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 92909 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+940.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 93910 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+950.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 94911 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+960.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 95911 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+970.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 96911 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+980.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 97911 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+990.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 98911 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 99912 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 100912 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 101912 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1030.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 102912 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223808 134559342 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1040.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 103912 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1050.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 104912 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1060.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 105912 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1070.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 106912 104 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1080.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 107912 105 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1090.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39541 0 0 0 108912 105 0 0 25 0 1 0 491841918 162398208 38872 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39648 38872 603 41 0 39607 0 vsize: 158592 [startup+1100.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 39723 0 0 0 109912 105 0 0 25 0 1 0 491841918 163213312 39054 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39847 39054 603 41 0 39806 0 vsize: 159388 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 40175 0 0 0 110911 106 0 0 25 0 1 0 491841918 165105664 39506 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 40309 39506 603 41 0 40268 0 vsize: 161236 [startup+1120.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 40596 0 0 0 111911 106 0 0 25 0 1 0 491841918 166719488 39927 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 40703 39927 603 41 0 40662 0 vsize: 162812 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 41312 0 0 0 112909 108 0 0 25 0 1 0 491841918 169664512 40643 4294967295 134512640 134672761 3221224624 3221223728 134560136 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 41422 40643 603 41 0 41381 0 vsize: 165688 [startup+1140.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 41783 0 0 0 113908 110 0 0 25 0 1 0 491841918 171671552 41114 4294967295 134512640 134672761 3221224624 3221223728 134559951 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 41912 41114 603 41 0 41871 0 vsize: 167648 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 42317 0 0 0 114907 110 0 0 25 0 1 0 491841918 173842432 41648 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 42442 41648 603 41 0 42401 0 vsize: 169768 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 42838 0 0 0 115907 111 0 0 25 0 1 0 491841918 175976448 42169 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 42963 42169 603 41 0 42922 0 vsize: 171852 [startup+1170.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 43376 0 0 0 116906 113 0 0 25 0 1 0 491841918 178126848 42707 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 43488 42707 603 41 0 43447 0 vsize: 173952 [startup+1180.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 44107 0 0 0 117904 114 0 0 25 0 1 0 491841918 181121024 43438 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 44219 43438 603 41 0 44178 0 vsize: 176876 [startup+1190.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 44837 0 0 0 118903 116 0 0 25 0 1 0 491841918 184107008 44168 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 44948 44168 603 41 0 44907 0 vsize: 179792 [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16224 Raw data (stat): 16224 (minisat+) R 16223 32461 32460 0 -1 0 45414 0 0 0 119901 118 0 0 25 0 1 0 491841918 186535936 44745 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 45541 44745 603 41 0 45500 0 vsize: 182164 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.14 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 16224 Raw data (stat): 16224 (minisat+) Z 16223 32461 32460 0 -1 12 45416 0 0 0 119901 126 0 0 25 0 1 0 491841918 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.14 CPU time (s): 1200.28 CPU user time (s): 1199.01 CPU system time (s): 1.26381 CPU usage (%): 100.012 Max. virtual memory (Kb): 182164 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####