Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mod010.opb |
MD5SUM | ef7064a9be2b712276f7b600af28e2b0 |
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.18 |
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 wulflinc10 THE 2005-04-21 13:18:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18642 boxname=wulflinc10 idbench=1434 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ef7064a9be2b712276f7b600af28e2b0 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-mod010.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-mod010.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-mod010.opb IDLAUNCH: 18642 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 743000 kB Buffers: 27804 kB Cached: 242020 kB SwapCached: 0 kB Active: 28176 kB Inactive: 244188 kB HighTotal: 131008 kB HighFree: 82264 kB LowTotal: 903652 kB LowFree: 660736 kB SwapTotal: 2097136 kB SwapFree: 2096784 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6412 kB Slab: 13888 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 13:38:57 (client local time) WITH STATUS 0 IN 1200.3 SECONDS stats: 18642 7 1200.3 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 | 112641 342501 | 37547 0 0 nan | 0.000 % | c | 100 | 112566 342248 | 41301 93 747 8.0 | 0.739 % | c | 251 | 112566 342248 | 45431 244 4453 18.2 | 0.739 % | c | 477 | 112566 342248 | 49975 470 15059 32.0 | 0.739 % | c | 819 | 112566 342248 | 54972 812 37441 46.1 | 0.739 % | c | 1331 | 112566 342248 | 60469 1324 71852 54.3 | 0.739 % | c | 2095 | 112566 342248 | 66516 2088 201139 96.3 | 0.739 % | c | 3235 | 112566 342248 | 73168 3228 326074 101.0 | 0.739 % | c | 4943 | 112537 342164 | 80485 4914 477218 97.1 | 0.751 % | c | 7505 | 112537 342164 | 88533 7476 1210959 162.0 | 0.751 % | c | 11350 | 112537 342164 | 97387 11321 1873735 165.5 | 0.751 % | c | 17116 | 112537 342164 | 107125 17087 3521450 206.1 | 0.751 % | c | 25767 | 112512 342081 | 117838 25734 4545362 176.6 | 0.767 % | c | 38741 | 112460 341924 | 129622 38597 6644314 172.1 | 0.783 % | c | 58202 | 112449 341881 | 142584 58057 12905884 222.3 | 0.791 % | c | 87396 | 112356 341607 | 156843 87217 24567040 281.7 | 0.823 % | c | 131185 | 112327 341502 | 172527 131001 48087197 367.1 | 0.840 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.93 0.98 0.93 2/54 32019 Raw data (stat): 32019 (runsolver) R 32018 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487170581 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0006 s] Raw data (loadavg): 0.94 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 5603 0 0 0 984 14 0 0 25 0 1 0 487170581 22962176 4934 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5606 4934 603 41 0 5565 0 vsize: 22424 [startup+20.0008 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 6117 0 0 0 1982 15 0 0 25 0 1 0 487170581 25116672 5448 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6132 5448 603 41 0 6091 0 vsize: 24528 [startup+30.0012 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 6674 0 0 0 2981 17 0 0 25 0 1 0 487170581 27410432 6005 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6692 6005 603 41 0 6651 0 vsize: 26768 [startup+40.0012 s] Raw data (loadavg): 0.96 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 7325 0 0 0 3979 18 0 0 25 0 1 0 487170581 30113792 6656 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7352 6656 603 41 0 7311 0 vsize: 29408 [startup+50.0018 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 8070 0 0 0 4977 20 0 0 25 0 1 0 487170581 33087488 7401 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8078 7401 603 41 0 8037 0 vsize: 32312 [startup+60.0018 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 8746 0 0 0 5974 22 0 0 25 0 1 0 487170581 35917824 8077 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8769 8077 603 41 0 8728 0 vsize: 35076 [startup+70.002 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 9387 0 0 0 6972 24 0 0 25 0 1 0 487170581 38502400 8718 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9400 8718 603 41 0 9359 0 vsize: 37600 [startup+80.0022 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 9867 0 0 0 7971 25 0 0 25 0 1 0 487170581 40521728 9198 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9893 9198 603 41 0 9852 0 vsize: 39572 [startup+90.0014 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 10255 0 0 0 8970 27 0 0 25 0 1 0 487170581 42131456 9586 4294967295 134512640 134672761 3221224544 3221223648 134560501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10286 9586 603 41 0 10245 0 vsize: 41144 [startup+100.001 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 10734 0 0 0 9968 28 0 0 25 0 1 0 487170581 44019712 10065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10747 10065 603 41 0 10706 0 vsize: 42988 [startup+110.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 11302 0 0 0 10967 30 0 0 25 0 1 0 487170581 46309376 10633 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11306 10633 603 41 0 11265 0 vsize: 45224 [startup+120.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 11737 0 0 0 11966 31 0 0 25 0 1 0 487170581 48189440 11068 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11765 11068 603 41 0 11724 0 vsize: 47060 [startup+130.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 12298 0 0 0 12965 32 0 0 25 0 1 0 487170581 50601984 11629 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12354 11629 603 41 0 12313 0 vsize: 49416 [startup+140.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 12777 0 0 0 13963 34 0 0 25 0 1 0 487170581 52486144 12108 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12814 12108 603 41 0 12773 0 vsize: 51256 [startup+150.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 13466 0 0 0 14962 36 0 0 25 0 1 0 487170581 55345152 12797 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13512 12797 603 41 0 13471 0 vsize: 54048 [startup+160.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 14006 0 0 0 15960 38 0 0 25 0 1 0 487170581 57495552 13337 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14037 13337 603 41 0 13996 0 vsize: 56148 [startup+170.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 14607 0 0 0 16958 40 0 0 25 0 1 0 487170581 59899904 13938 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14624 13938 603 41 0 14583 0 vsize: 58496 [startup+180.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 15192 0 0 0 17957 41 0 0 25 0 1 0 487170581 62308352 14523 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15212 14523 603 41 0 15171 0 vsize: 60848 [startup+190.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 15829 0 0 0 18955 43 0 0 25 0 1 0 487170581 64991232 15160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15867 15160 603 41 0 15826 0 vsize: 63468 [startup+200.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 16615 0 0 0 19953 46 0 0 25 0 1 0 487170581 68165632 15946 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16642 15946 603 41 0 16601 0 vsize: 66568 [startup+210.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 17233 0 0 0 20951 48 0 0 25 0 1 0 487170581 70717440 16564 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17265 16564 603 41 0 17224 0 vsize: 69060 [startup+220.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 17858 0 0 0 21949 50 0 0 25 0 1 0 487170581 73273344 17189 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17889 17189 603 41 0 17848 0 vsize: 71556 [startup+230.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 18387 0 0 0 22948 51 0 0 25 0 1 0 487170581 75440128 17718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18418 17718 603 41 0 18377 0 vsize: 73672 [startup+240.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 18873 0 0 0 23947 53 0 0 25 0 1 0 487170581 77332480 18204 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18880 18204 603 41 0 18839 0 vsize: 75520 [startup+250.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 19420 0 0 0 24945 54 0 0 25 0 1 0 487170581 79613952 18751 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19437 18751 603 41 0 19396 0 vsize: 77748 [startup+260.001 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 20136 0 0 0 25943 57 0 0 25 0 1 0 487170581 82587648 19467 4294967295 134512640 134672761 3221224544 3221223648 134559958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20163 19467 603 41 0 20122 0 vsize: 80652 [startup+270.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 20912 0 0 0 26941 59 0 0 25 0 1 0 487170581 85688320 20243 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20920 20243 603 41 0 20879 0 vsize: 83680 [startup+280.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 21603 0 0 0 27939 61 0 0 25 0 1 0 487170581 88481792 20934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21602 20934 603 41 0 21561 0 vsize: 86408 [startup+290.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 22417 0 0 0 28937 63 0 0 25 0 1 0 487170581 92119040 21748 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22490 21748 603 41 0 22449 0 vsize: 89960 [startup+300.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 23003 0 0 0 29935 65 0 0 25 0 1 0 487170581 94556160 22334 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23085 22334 603 41 0 23044 0 vsize: 92340 [startup+310.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 23688 0 0 0 30934 67 0 0 25 0 1 0 487170581 97370112 23019 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23772 23019 603 41 0 23731 0 vsize: 95088 [startup+320.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 24331 0 0 0 31932 68 0 0 25 0 1 0 487170581 99946496 23662 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24401 23662 603 41 0 24360 0 vsize: 97604 [startup+330.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 25105 0 0 0 32931 70 0 0 25 0 1 0 487170581 103067648 24436 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25163 24436 603 41 0 25122 0 vsize: 100652 [startup+340.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 25669 0 0 0 33929 72 0 0 25 0 1 0 487170581 105361408 25000 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25723 25000 603 41 0 25682 0 vsize: 102892 [startup+350.002 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 26280 0 0 0 34928 74 0 0 25 0 1 0 487170581 107917312 25611 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26347 25611 603 41 0 26306 0 vsize: 105388 [startup+360.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 26790 0 0 0 35926 76 0 0 25 0 1 0 487170581 109940736 26121 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26841 26121 603 41 0 26800 0 vsize: 107364 [startup+370.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 27328 0 0 0 36925 77 0 0 25 0 1 0 487170581 112234496 26659 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27401 26659 603 41 0 27360 0 vsize: 109604 [startup+380.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 27761 0 0 0 37925 78 0 0 25 0 1 0 487170581 113991680 27092 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27830 27092 603 41 0 27789 0 vsize: 111320 [startup+390.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 28174 0 0 0 38924 79 0 0 25 0 1 0 487170581 115609600 27505 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28225 27505 603 41 0 28184 0 vsize: 112900 [startup+400.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 28862 0 0 0 39921 81 0 0 25 0 1 0 487170581 118444032 28193 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28917 28193 603 41 0 28876 0 vsize: 115668 [startup+410.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 29560 0 0 0 40920 83 0 0 25 0 1 0 487170581 121282560 28891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29610 28891 603 41 0 29569 0 vsize: 118440 [startup+420.003 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 30245 0 0 0 41918 85 0 0 25 0 1 0 487170581 124108800 29576 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30300 29576 603 41 0 30259 0 vsize: 121200 [startup+430.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 30812 0 0 0 42916 87 0 0 25 0 1 0 487170581 126382080 30143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30855 30143 603 41 0 30814 0 vsize: 123420 [startup+440.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 31335 0 0 0 43915 88 0 0 25 0 1 0 487170581 128540672 30666 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31382 30666 603 41 0 31341 0 vsize: 125528 [startup+450.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 32022 0 0 0 44913 89 0 0 25 0 1 0 487170581 131383296 31353 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32076 31353 603 41 0 32035 0 vsize: 128304 [startup+460.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 32246 0 0 0 45913 90 0 0 25 0 1 0 487170581 132329472 31577 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32307 31577 603 41 0 32266 0 vsize: 129228 [startup+470.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 32752 0 0 0 46912 90 0 0 25 0 1 0 487170581 134352896 32083 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32801 32083 603 41 0 32760 0 vsize: 131204 [startup+480.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 33341 0 0 0 47911 92 0 0 25 0 1 0 487170581 136773632 32672 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33392 32672 603 41 0 33351 0 vsize: 133568 [startup+490.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 33909 0 0 0 48910 93 0 0 25 0 1 0 487170581 139055104 33240 4294967295 134512640 134672761 3221224544 3221223648 134559969 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33949 33240 603 41 0 33908 0 vsize: 135796 [startup+500.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 34510 0 0 0 49908 95 0 0 25 0 1 0 487170581 141598720 33841 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34570 33841 603 41 0 34529 0 vsize: 138280 [startup+510.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 35091 0 0 0 50906 97 0 0 25 0 1 0 487170581 143892480 34422 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35130 34422 603 41 0 35089 0 vsize: 140520 [startup+520.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 35854 0 0 0 51905 98 0 0 25 0 1 0 487170581 146997248 35185 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35888 35185 603 41 0 35847 0 vsize: 143552 [startup+530.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 36515 0 0 0 52904 100 0 0 25 0 1 0 487170581 149696512 35846 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 36547 35846 603 41 0 36506 0 vsize: 146188 [startup+540.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 37201 0 0 0 53902 102 0 0 25 0 1 0 487170581 152588288 36532 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37253 36532 603 41 0 37212 0 vsize: 149012 [startup+550.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 37648 0 0 0 54901 103 0 0 25 0 1 0 487170581 154333184 36979 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37679 36979 603 41 0 37638 0 vsize: 150716 [startup+560.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 38107 0 0 0 55900 105 0 0 25 0 1 0 487170581 156217344 37438 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 38139 37438 603 41 0 38098 0 vsize: 152556 [startup+570.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 38580 0 0 0 56899 106 0 0 25 0 1 0 487170581 158109696 37911 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 38601 37911 603 41 0 38560 0 vsize: 154404 [startup+580.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 38956 0 0 0 57898 106 0 0 25 0 1 0 487170581 159735808 38287 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 38998 38287 603 41 0 38957 0 vsize: 155992 [startup+590.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 39598 0 0 0 58897 108 0 0 25 0 1 0 487170581 162263040 38929 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39615 38929 603 41 0 39574 0 vsize: 158460 [startup+600.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 40215 0 0 0 59895 110 0 0 25 0 1 0 487170581 164810752 39546 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 40237 39546 603 41 0 40196 0 vsize: 160948 [startup+610.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 40811 0 0 0 60894 111 0 0 25 0 1 0 487170581 167223296 40142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 40826 40142 603 41 0 40785 0 vsize: 163304 [startup+620.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 41453 0 0 0 61894 112 0 0 25 0 1 0 487170581 169885696 40784 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 41476 40784 603 41 0 41435 0 vsize: 165904 [startup+630.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 42074 0 0 0 62892 114 0 0 25 0 1 0 487170581 172429312 41405 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 42097 41405 603 41 0 42056 0 vsize: 168388 [startup+640.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 42572 0 0 0 63891 115 0 0 25 0 1 0 487170581 174432256 41903 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 42586 41903 603 41 0 42545 0 vsize: 170344 [startup+650.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 43288 0 0 0 64889 117 0 0 25 0 1 0 487170581 177397760 42619 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 43310 42619 603 41 0 43269 0 vsize: 173240 [startup+660.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 44009 0 0 0 65888 118 0 0 25 0 1 0 487170581 180363264 43340 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 44034 43340 603 41 0 43993 0 vsize: 176136 [startup+670.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 44721 0 0 0 66886 121 0 0 25 0 1 0 487170581 183320576 44052 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 44756 44052 603 41 0 44715 0 vsize: 179024 [startup+680.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 45392 0 0 0 67884 123 0 0 25 0 1 0 487170581 186036224 44723 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 45419 44723 603 41 0 45378 0 vsize: 181676 [startup+690.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 46046 0 0 0 68882 124 0 0 25 0 1 0 487170581 188743680 45377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 46080 45377 603 41 0 46039 0 vsize: 184320 [startup+700.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 46685 0 0 0 69881 126 0 0 25 0 1 0 487170581 191291392 46016 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 46702 46016 603 41 0 46661 0 vsize: 186808 [startup+710.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 47294 0 0 0 70881 126 0 0 25 0 1 0 487170581 193851392 46625 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 47327 46625 603 41 0 47286 0 vsize: 189308 [startup+720.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 47895 0 0 0 71880 127 0 0 25 0 1 0 487170581 196284416 47226 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 47921 47226 603 41 0 47880 0 vsize: 191684 [startup+730.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 48537 0 0 0 72879 128 0 0 25 0 1 0 487170581 198844416 47868 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 48546 47868 603 41 0 48505 0 vsize: 194184 [startup+740.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 49172 0 0 0 73877 131 0 0 25 0 1 0 487170581 201555968 48503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 49208 48503 603 41 0 49167 0 vsize: 196832 [startup+750.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 49789 0 0 0 74876 132 0 0 25 0 1 0 487170581 204005376 49120 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 49806 49120 603 41 0 49765 0 vsize: 199224 [startup+760.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 50410 0 0 0 75874 134 0 0 25 0 1 0 487170581 206565376 49741 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 50431 49741 603 41 0 50390 0 vsize: 201724 [startup+770.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 51006 0 0 0 76873 135 0 0 25 0 1 0 487170581 209002496 50337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 51026 50337 603 41 0 50985 0 vsize: 204104 [startup+780.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 51603 0 0 0 77872 137 0 0 25 0 1 0 487170581 211546112 50934 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 51647 50934 603 41 0 51606 0 vsize: 206588 [startup+790.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 52219 0 0 0 78870 139 0 0 25 0 1 0 487170581 213975040 51550 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 52240 51550 603 41 0 52199 0 vsize: 208960 [startup+800.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 52797 0 0 0 79869 140 0 0 25 0 1 0 487170581 216416256 52128 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 52836 52128 603 41 0 52795 0 vsize: 211344 [startup+810.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 53414 0 0 0 80868 141 0 0 25 0 1 0 487170581 218841088 52745 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 53428 52745 603 41 0 53387 0 vsize: 213712 [startup+820.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 53998 0 0 0 81866 143 0 0 25 0 1 0 487170581 221265920 53329 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 54020 53329 603 41 0 53979 0 vsize: 216080 [startup+830.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 54577 0 0 0 82864 145 0 0 25 0 1 0 487170581 224215040 53908 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 54740 53908 603 41 0 54699 0 vsize: 218960 [startup+840.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 55280 0 0 0 83861 148 0 0 25 0 1 0 487170581 227008512 54611 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 55422 54611 603 41 0 55381 0 vsize: 221688 [startup+850.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 55722 0 0 0 84860 150 0 0 25 0 1 0 487170581 228880384 55053 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 55879 55053 603 41 0 55838 0 vsize: 223516 [startup+860.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 56084 0 0 0 85859 150 0 0 25 0 1 0 487170581 230350848 55415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 56238 55415 603 41 0 56197 0 vsize: 224952 [startup+870.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 56326 0 0 0 86859 151 0 0 25 0 1 0 487170581 231280640 55657 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 56465 55657 603 41 0 56424 0 vsize: 225860 [startup+880.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 56816 0 0 0 87858 152 0 0 25 0 1 0 487170581 233299968 56147 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 56958 56147 603 41 0 56917 0 vsize: 227832 [startup+890.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 57470 0 0 0 88857 154 0 0 25 0 1 0 487170581 235986944 56801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 57614 56801 603 41 0 57573 0 vsize: 230456 [startup+900.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 58145 0 0 0 89855 155 0 0 25 0 1 0 487170581 238817280 57476 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 58305 57476 603 41 0 58264 0 vsize: 233220 [startup+910.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 58632 0 0 0 90854 157 0 0 25 0 1 0 487170581 240717824 57963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 58769 57963 603 41 0 58728 0 vsize: 235076 [startup+920.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 58891 0 0 0 91854 157 0 0 25 0 1 0 487170581 241795072 58222 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 59032 58222 603 41 0 58991 0 vsize: 236128 [startup+930.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 59350 0 0 0 92853 158 0 0 25 0 1 0 487170581 243679232 58681 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 59492 58681 603 41 0 59451 0 vsize: 237968 [startup+940.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 59441 0 0 0 93853 158 0 0 25 0 1 0 487170581 244084736 58772 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 59591 58772 603 41 0 59550 0 vsize: 238364 [startup+950.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 60002 0 0 0 94851 160 0 0 25 0 1 0 487170581 246407168 59333 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 60158 59333 603 41 0 60117 0 vsize: 240632 [startup+960.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 60369 0 0 0 95851 161 0 0 25 0 1 0 487170581 247889920 59700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 60520 59700 603 41 0 60479 0 vsize: 242080 [startup+970.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 60802 0 0 0 96850 162 0 0 25 0 1 0 487170581 249638912 60133 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 60947 60133 603 41 0 60906 0 vsize: 243788 [startup+980.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 61449 0 0 0 97848 164 0 0 25 0 1 0 487170581 252313600 60780 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 61600 60780 603 41 0 61559 0 vsize: 246400 [startup+990.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 62047 0 0 0 98846 166 0 0 25 0 1 0 487170581 254746624 61378 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 62194 61378 603 41 0 62153 0 vsize: 248776 [startup+1000.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 62474 0 0 0 99845 167 0 0 25 0 1 0 487170581 256499712 61805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 62622 61805 603 41 0 62581 0 vsize: 250488 [startup+1010.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 62865 0 0 0 100844 169 0 0 25 0 1 0 487170581 257982464 62196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 62984 62196 603 41 0 62943 0 vsize: 251936 [startup+1020.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 63272 0 0 0 101844 169 0 0 25 0 1 0 487170581 259723264 62603 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 63409 62603 603 41 0 63368 0 vsize: 253636 [startup+1030.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 63761 0 0 0 102842 171 0 0 25 0 1 0 487170581 261718016 63092 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 63896 63092 603 41 0 63855 0 vsize: 255584 [startup+1040.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 64352 0 0 0 103841 172 0 0 25 0 1 0 487170581 264069120 63683 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 64470 63683 603 41 0 64429 0 vsize: 257880 [startup+1050.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 64928 0 0 0 104839 174 0 0 25 0 1 0 487170581 266452992 64259 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 65052 64259 603 41 0 65011 0 vsize: 260208 [startup+1060.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 65483 0 0 0 105838 175 0 0 25 0 1 0 487170581 268718080 64814 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 65605 64814 603 41 0 65564 0 vsize: 262420 [startup+1070.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 65796 0 0 0 106838 176 0 0 25 0 1 0 487170581 270036992 65127 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 65927 65127 603 41 0 65886 0 vsize: 263708 [startup+1080.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 65912 0 0 0 107837 177 0 0 25 0 1 0 487170581 270438400 65243 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66025 65243 603 41 0 65984 0 vsize: 264100 [startup+1090.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 66435 0 0 0 108836 178 0 0 25 0 1 0 487170581 272592896 65766 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66551 65766 603 41 0 66510 0 vsize: 266204 [startup+1100.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 66962 0 0 0 109835 179 0 0 25 0 1 0 487170581 274743296 66293 4294967295 134512640 134672761 3221224544 3221223648 134559958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67076 66293 603 41 0 67035 0 vsize: 268304 [startup+1110.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 67457 0 0 0 110833 181 0 0 25 0 1 0 487170581 276770816 66788 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67571 66788 603 41 0 67530 0 vsize: 270284 [startup+1120.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 67931 0 0 0 111832 183 0 0 25 0 1 0 487170581 278794240 67262 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68065 67262 603 41 0 68024 0 vsize: 272260 [startup+1130.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 68244 0 0 0 112832 183 0 0 25 0 1 0 487170581 280014848 67575 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68363 67575 603 41 0 68322 0 vsize: 273452 [startup+1140.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 68782 0 0 0 113830 185 0 0 25 0 1 0 487170581 282284032 68113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68917 68113 603 41 0 68876 0 vsize: 275668 [startup+1150.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 69265 0 0 0 114829 186 0 0 25 0 1 0 487170581 284147712 68596 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 69372 68596 603 41 0 69331 0 vsize: 277488 [startup+1160.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 69770 0 0 0 115828 188 0 0 25 0 1 0 487170581 286289920 69101 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 69895 69101 603 41 0 69854 0 vsize: 279580 [startup+1170.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 70215 0 0 0 116826 190 0 0 25 0 1 0 487170581 288030720 69546 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 70320 69546 603 41 0 70279 0 vsize: 281280 [startup+1180.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 70602 0 0 0 117825 191 0 0 25 0 1 0 487170581 289648640 69933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 70715 69933 603 41 0 70674 0 vsize: 282860 [startup+1190.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 70835 0 0 0 118825 192 0 0 25 0 1 0 487170581 290598912 70166 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 70947 70166 603 41 0 70906 0 vsize: 283788 [startup+1200.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 32019 Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 71108 0 0 0 119824 192 0 0 25 0 1 0 487170581 291672064 70439 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 71209 70439 603 41 0 71168 0 vsize: 284836 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.14 s] Raw data (loadavg): 0.99 0.98 0.93 1/54 32019 Raw data (stat): 32019 (minisat+) Z 32018 25347 25346 0 -1 12 71110 0 0 0 119824 205 0 0 25 0 1 0 487170581 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.3 CPU user time (s): 1198.25 CPU system time (s): 2.05569 CPU usage (%): 100.013 Max. virtual memory (Kb): 284836 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####