Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32e5.opb |
MD5SUM | 6caf33eeba2c45b0896a04cb80501c4f |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 503 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1044 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1044 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1044 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 312.97 |
Number of variables | 1044 |
Total number of constraints | 12158 |
Number of constraints which are clauses | 12158 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 32 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc29 THE 2005-04-14 00:13:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3922 boxname=wulflinc29 idbench=162 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6caf33eeba2c45b0896a04cb80501c4f /oldhome/oroussel/tmp/wulflinc29/normalized-ii32e5.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-ii32e5.opb /oldhome/oroussel/tmp/wulflinc29/normalized-ii32e5.opb IDLAUNCH: 3922 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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 : 3 cpu MHz : 451.020 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: 832136 kB Buffers: 35908 kB Cached: 129048 kB SwapCached: 12 kB Active: 53408 kB Inactive: 114412 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 831884 kB SwapTotal: 2097892 kB SwapFree: 2097880 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 28980 kB Committed_AS: 63472 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 00:26:50 (client local time) WITH STATUS 30 IN 827.273 SECONDS stats: 3922 0 827.273 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 12158 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 12158 50526 | 3647 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/1044 c -- var.elim.: 1044/1044 c | 0 | 12158 50526 | 4863 0 0 nan | 0.000 % | c | 100 | 12158 50526 | 5349 100 4505 45.0 | 0.010 % | c ============================================================================== c (current CPU-time: 0.763883 s) c ============================================================================== c [1mFound solution: 504[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:57176 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 165 | 79804 208715 | 23941 165 8627 52.3 | 0.010 % | c -- subsuming c -- var.elim.: 1000/45300 c -- var.elim.: 2000/45300 c -- var.elim.: 3000/45300 c -- var.elim.: 4000/45300 c -- var.elim.: 5000/45300 c -- var.elim.: 6000/45300 c -- var.elim.: 7000/45300 c -- var.elim.: 8000/45300 c -- var.elim.: 9000/45300 c -- var.elim.: 10000/45300 c -- var.elim.: 11000/45300 c -- var.elim.: 12000/45300 c -- var.elim.: 13000/45300 c -- var.elim.: 14000/45300 c -- var.elim.: 15000/45300 c -- var.elim.: 16000/45300 c -- var.elim.: 17000/45300 c -- var.elim.: 18000/45300 c -- var.elim.: 19000/45300 c -- var.elim.: 20000/45300 c -- var.elim.: 21000/45300 c -- var.elim.: 22000/45300 c -- var.elim.: 23000/45300 c -- var.elim.: 24000/45300 c -- var.elim.: 25000/45300 c -- var.elim.: 26000/45300 c -- var.elim.: 27000/45300 c -- var.elim.: 28000/45300 c -- var.elim.: 29000/45300 c -- var.elim.: 30000/45300 c -- var.elim.: 31000/45300 c -- var.elim.: 32000/45300 c -- var.elim.: 33000/45300 c -- var.elim.: 34000/45300 c -- var.elim.: 35000/45300 c -- var.elim.: 36000/45300 c -- var.elim.: 37000/45300 c -- var.elim.: 38000/45300 c -- var.elim.: 39000/45300 c -- var.elim.: 40000/45300 c -- var.elim.: 41000/45300 c -- var.elim.: 42000/45300 c -- var.elim.: 43000/45300 c -- var.elim.: 44000/45300 c -- var.elim.: 45000/45300 c -- var.elim.: 45300/45300 c -- var.elim.: 1000/22464 c -- var.elim.: 2000/22464 c -- var.elim.: 3000/22464 c -- var.elim.: 4000/22464 c -- var.elim.: 5000/22464 c -- var.elim.: 6000/22464 c -- var.elim.: 7000/22464 c -- var.elim.: 8000/22464 c -- var.elim.: 9000/22464 c -- var.elim.: 10000/22464 c -- var.elim.: 11000/22464 c -- var.elim.: 12000/22464 c -- var.elim.: 13000/22464 c -- var.elim.: 14000/22464 c -- var.elim.: 15000/22464 c -- var.elim.: 16000/22464 c -- var.elim.: 17000/22464 c -- var.elim.: 18000/22464 c -- var.elim.: 19000/22464 c -- var.elim.: 20000/22464 c -- var.elim.: 21000/22464 c -- var.elim.: 22000/22464 c -- var.elim.: 22464/22464 c -- var.elim.: 1000/13898 c -- var.elim.: 2000/13898 c -- var.elim.: 3000/13898 c -- var.elim.: 4000/13898 c -- var.elim.: 5000/13898 c -- var.elim.: 6000/13898 c -- var.elim.: 7000/13898 c -- var.elim.: 8000/13898 c -- var.elim.: 9000/13898 c -- var.elim.: 10000/13898 c -- var.elim.: 11000/13898 c -- var.elim.: 12000/13898 c -- var.elim.: 13000/13898 c -- var.elim.: 13898/13898 c -- var.elim.: 1000/10121 c -- var.elim.: 2000/10121 c -- var.elim.: 3000/10121 c -- var.elim.: 4000/10121 c -- var.elim.: 5000/10121 c -- var.elim.: 6000/10121 c -- var.elim.: 7000/10121 c -- var.elim.: 8000/10121 c -- var.elim.: 9000/10121 c -- var.elim.: 10000/10121 c -- var.elim.: 10121/10121 c -- var.elim.: 1000/7631 c -- var.elim.: 2000/7631 c -- var.elim.: 3000/7631 c -- var.elim.: 4000/7631 c -- var.elim.: 5000/7631 c -- var.elim.: 6000/7631 c -- var.elim.: 7000/7631 c -- var.elim.: 7631/7631 c -- var.elim.: 1000/6808 c -- var.elim.: 2000/6808 c -- var.elim.: 3000/6808 c -- var.elim.: 4000/6808 c -- var.elim.: 5000/6808 c -- var.elim.: 6000/6808 c -- var.elim.: 6808/6808 c -- var.elim.: 1000/5945 c -- var.elim.: 2000/5945 c -- var.elim.: 3000/5945 c -- var.elim.: 4000/5945 c -- var.elim.: 5000/5945 c -- var.elim.: 5945/5945 c -- var.elim.: 1000/5432 c -- var.elim.: 2000/5432 c -- var.elim.: 3000/5432 c -- var.elim.: 4000/5432 c -- var.elim.: 5000/5432 c -- var.elim.: 5432/5432 c -- var.elim.: 1000/4776 c -- var.elim.: 2000/4776 c -- var.elim.: 3000/4776 c -- var.elim.: 4000/4776 c -- var.elim.: 4776/4776 c -- var.elim.: 330/330 c -- subsuming c -- var.elim.: 1000/7057 c -- var.elim.: 2000/7057 c -- var.elim.: 3000/7057 c -- var.elim.: 4000/7057 c -- var.elim.: 5000/7057 c -- var.elim.: 6000/7057 c -- var.elim.: 7000/7057 c -- var.elim.: 7057/7057 c -- var.elim.: 172/172 c | 165 | 30725 212022 | -- 165 -- -- | -- | -49060/3372 c | 165 | 30725 212022 | 12290 165 8627 52.3 | 0.010 % | c | 269 | 30725 212022 | 13519 269 14300 53.2 | 0.195 % | c | 421 | 30725 212022 | 14870 421 23083 54.8 | 0.195 % | c | 646 | 30725 212022 | 16357 646 34392 53.2 | 0.195 % | c | 986 | 30725 212022 | 17993 986 347941 352.9 | 0.195 % | c | 1494 | 30725 212022 | 19793 1494 643363 430.6 | 0.195 % | c ============================================================================== c (current CPU-time: 179.654 s) c ============================================================================== c [1mFound solution: 503[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2013 | 77812 327560 | 23343 2013 1161789 577.1 | 0.195 % | c -- subsuming c -- var.elim.: 1000/43002 c -- var.elim.: 2000/43002 c -- var.elim.: 3000/43002 c -- var.elim.: 4000/43002 c -- var.elim.: 5000/43002 c -- var.elim.: 6000/43002 c -- var.elim.: 7000/43002 c -- var.elim.: 8000/43002 c -- var.elim.: 9000/43002 c -- var.elim.: 10000/43002 c -- var.elim.: 11000/43002 c -- var.elim.: 12000/43002 c -- var.elim.: 13000/43002 c -- var.elim.: 14000/43002 c -- var.elim.: 15000/43002 c -- var.elim.: 16000/43002 c -- var.elim.: 17000/43002 c -- var.elim.: 18000/43002 c -- var.elim.: 19000/43002 c -- var.elim.: 20000/43002 c -- var.elim.: 21000/43002 c -- var.elim.: 22000/43002 c -- var.elim.: 23000/43002 c -- var.elim.: 24000/43002 c -- var.elim.: 25000/43002 c -- var.elim.: 26000/43002 c -- var.elim.: 27000/43002 c -- var.elim.: 28000/43002 c -- var.elim.: 29000/43002 c -- var.elim.: 30000/43002 c -- var.elim.: 31000/43002 c -- var.elim.: 32000/43002 c -- var.elim.: 33000/43002 c -- var.elim.: 34000/43002 c -- var.elim.: 35000/43002 c -- var.elim.: 36000/43002 c -- var.elim.: 37000/43002 c -- var.elim.: 38000/43002 c -- var.elim.: 39000/43002 c -- var.elim.: 40000/43002 c -- var.elim.: 41000/43002 c -- var.elim.: 42000/43002 c -- var.elim.: 43000/43002 c -- var.elim.: 43002/43002 c -- var.elim.: 1000/20811 c -- var.elim.: 2000/20811 c -- var.elim.: 3000/20811 c -- var.elim.: 4000/20811 c -- var.elim.: 5000/20811 c -- var.elim.: 6000/20811 c -- var.elim.: 7000/20811 c -- var.elim.: 8000/20811 c -- var.elim.: 9000/20811 c -- var.elim.: 10000/20811 c -- var.elim.: 11000/20811 c -- var.elim.: 12000/20811 c -- var.elim.: 13000/20811 c -- var.elim.: 14000/20811 c -- var.elim.: 15000/20811 c -- var.elim.: 16000/20811 c -- var.elim.: 17000/20811 c -- var.elim.: 18000/20811 c -- var.elim.: 19000/20811 c -- var.elim.: 20000/20811 c -- var.elim.: 20811/20811 c -- var.elim.: 1000/12809 c -- var.elim.: 2000/12809 c -- var.elim.: 3000/12809 c -- var.elim.: 4000/12809 c -- var.elim.: 5000/12809 c -- var.elim.: 6000/12809 c -- var.elim.: 7000/12809 c -- var.elim.: 8000/12809 c -- var.elim.: 9000/12809 c -- var.elim.: 10000/12809 c -- var.elim.: 11000/12809 c -- var.elim.: 12000/12809 c -- var.elim.: 12809/12809 c -- var.elim.: 1000/10267 c -- var.elim.: 2000/10267 c -- var.elim.: 3000/10267 c -- var.elim.: 4000/10267 c -- var.elim.: 5000/10267 c -- var.elim.: 6000/10267 c -- var.elim.: 7000/10267 c -- var.elim.: 8000/10267 c -- var.elim.: 9000/10267 c -- var.elim.: 10000/10267 c -- var.elim.: 10267/10267 c -- var.elim.: 1000/8702 c -- var.elim.: 2000/8702 c -- var.elim.: 3000/8702 c -- var.elim.: 4000/8702 c -- var.elim.: 5000/8702 c -- var.elim.: 6000/8702 c -- var.elim.: 7000/8702 c -- var.elim.: 8000/8702 c -- var.elim.: 8702/8702 c -- var.elim.: 1000/7483 c -- var.elim.: 2000/7483 c -- var.elim.: 3000/7483 c -- var.elim.: 4000/7483 c -- var.elim.: 5000/7483 c -- var.elim.: 6000/7483 c -- var.elim.: 7000/7483 c -- var.elim.: 7483/7483 c -- var.elim.: 1000/5997 c -- var.elim.: 2000/5997 c -- var.elim.: 3000/5997 c -- var.elim.: 4000/5997 c -- var.elim.: 5000/5997 c -- var.elim.: 5997/5997 c -- var.elim.: 1000/4274 c -- var.elim.: 2000/4274 c -- var.elim.: 3000/4274 c -- var.elim.: 4000/4274 c -- var.elim.: 4274/4274 c -- var.elim.: 1000/1064 c -- var.elim.: 1064/1064 c -- subsuming c -- var.elim.: 271/271 c -- var.elim.: 105/105 c | 2013 | 30749 212516 | -- 2013 -- -- | -- | -47063/-115043 c | 2013 | 30749 212516 | 12299 1811 535765 295.8 | 0.195 % | c | 2115 | 30749 212516 | 13529 1913 655855 342.8 | 0.205 % | c | 2265 | 30749 212516 | 14882 2063 729804 353.8 | 0.205 % | c | 2493 | 30749 212516 | 16370 2291 887834 387.5 | 0.205 % | c | 2832 | 30749 212516 | 18007 2630 907170 344.9 | 0.205 % | c | 3338 | 30749 212516 | 19808 3136 933249 297.6 | 0.205 % | c | 4098 | 30749 212516 | 21789 3896 1142810 293.3 | 0.205 % | c | 5238 | 30733 212401 | 23955 5035 2023813 401.9 | 0.256 % | c | 6947 | 30733 212401 | 26351 6744 4241404 628.9 | 0.256 % | c | 9510 | 30717 212268 | 28971 9306 6828452 733.8 | 0.317 % | c | 13354 | 30717 212268 | 31868 13150 10878729 827.3 | 0.317 % | c | 19125 | 30717 212268 | 35055 18921 19493328 1030.2 | 0.317 % | c | 27774 | 30688 212078 | 38524 27569 31845688 1155.1 | 0.440 % | c | 40748 | 30688 212078 | 42377 16304 16199028 993.6 | 0.440 % | c | 60209 | 30628 211646 | 46523 35763 40120853 1121.9 | 0.706 % | c ============================================================================== c [1mOptimal solution: 503[0m s OPTIMUM FOUND v x1 -x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 -x15 -x16 x17 -x18 -x19 -x20 -x21 x22 x23 -x24 x25 -x26 -x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 -x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 -x59 -x60 -x61 x62 x63 -x64 -x65 -x66 x67 -x68 x69 -x70 -x71 -x72 -x73 -x74 x75 -x76 x77 -x78 x79 -x80 -x81 -x82 x83 -x84 x85 -x86 -x87 -x88 x89 -x90 -x91 -x92 x93 -x94 -x95 x96 -x97 -x98 x99 -x100 x101 -x102 -x103 x104 x105 -x106 -x107 -x108 x109 -x110 x111 -x112 x113 -x114 -x115 -x116 x117 -x118 x119 -x120 -x121 -x122 x123 -x124 x125 -x126 -x127 -x128 x129 -x130 x131 -x132 -x133 x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 x201 -x202 x203 -x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 -x241 x242 x243 -x244 x245 -x246 x247 -x248 x249 -x250 -x251 x252 x253 -x254 x255 -x256 x257 -x258 x259 -x260 x261 -x262 x263 -x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 -x289 x290 x291 -x292 -x293 x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 x317 -x318 x319 -x320 x321 -x322 x323 -x324 x325 -x326 x327 -x328 x329 -x330 x331 -x332 x333 -x334 x335 -x336 x337 -x338 x339 -x340 x341 -x342 x343 -x344 -x345 x346 x347 -x348 x349 -x350 x351 -x352 x353 -x354 x355 -x356 x357 -x358 x359 -x360 x361 -x362 x363 -x364 x365 -x366 x367 -x368 x369 -x370 x371 -x372 x373 -x374 x375 -x376 x377 -x378 x379 -x380 x381 -x382 x383 -x384 -x385 x386 x387 -x388 -x389 x390 -x391 x392 -x393 x394 x395 -x396 -x397 x398 x399 -x400 -x401 x402 -x403 x404 x405 -x406 -x407 -x408 -x409 x410 -x411 x412 x413 -x414 -x415 x416 x417 -x418 -x419 x420 -x421 x422 -x423 x424 x425 -x426 -x427 x428 x429 -x430 -x431 x432 -x433 x434 x435 -x436 -x437 x438 -x439 x440 x441 -x442 -x443 x444 x445 -x446 -x447 x448 -x449 x450 -x451 x452 -x453 x454 x455 -x456 -x457 x458 x459 -x460 -x461 x462 -x463 x464 -x465 x466 x467 -x468 -x469 x470 -x471 x472 x473 -x474 -x475 x476 x477 -x478 -x479 x480 -x481 x482 -x483 x484 x485 -x486 -x487 x488 -x489 x490 x491 -x492 -x493 x494 x495 -x496 -x497 x498 -x499 x500 -x501 x502 x503 -x504 -x505 x506 -x507 x508 x509 -x510 -x511 x512 -x513 x514 x515 -x516 -x517 x518 x519 -x520 -x521 x522 -x523 x524 x525 -x526 -x527 x528 -x529 x530 x531 -x532 -x533 x534 -x535 x536 x537 -x538 -x539 x540 -x541 x542 -x543 x544 x545 -x546 -x547 x548 -x549 x550 x551 -x552 -x553 x554 -x555 x556 x557 -x558 -x559 x560 x561 -x562 -x563 x564 -x565 x566 x567 -x568 -x569 x570 -x571 x572 x573 -x574 -x575 x576 -x577 x578 x579 -x580 -x581 x582 -x583 x584 x585 -x586 -x587 x588 -x589 x590 x591 -x592 -x593 x594 -x595 x596 x597 -x598 -x599 x600 -x601 x602 x603 -x604 -x605 x606 -x607 x608 -x609 x610 x611 -x612 -x613 x614 -x615 x616 x617 -x618 -x619 x620 x621 -x622 -x623 x624 -x625 x626 x627 -x628 -x629 x630 -x631 x632 x633 -x634 -x635 x636 -x637 x638 -x639 x640 x641 -x642 -x643 x644 -x645 x646 x647 -x648 -x649 x650 -x651 x652 x653 -x654 -x655 x656 -x657 x658 x659 -x660 -x661 x662 -x663 x664 x665 -x666 -x667 x668 x669 -x670 -x671 x672 -x673 x674 x675 -x676 -x677 x678 -x679 x680 x681 -x682 -x683 x684 -x685 x686 -x687 x688 x689 -x690 -x691 x692 x693 -x694 -x695 x696 -x697 x698 x699 -x700 -x701 x702 -x703 x704 x705 -x706 -x707 x708 -x709 x710 x711 -x712 -x713 x714 -x715 x716 -x717 x718 x719 -x720 x721 -x722 -x723 x724 -x725 x726 -x727 x728 x729 -x730 -x731 x732 -x733 x734 x735 -x736 -x737 x738 -x739 x740 -x741 x742 x743 -x744 -x745 x746 -x747 x748 x749 -x750 -x751 x752 -x753 -x754 x755 -x756 -x757 x758 x759 -x760 -x761 x762 -x763 x764 x765 -x766 -x767 x768 -x769 x770 -x771 x772 x773 -x774 -x775 x776 x777 -x778 -x779 x780 -x781 x782 x783 -x784 -x785 -x786 -x787 x788 -x789 x790 x791 -x792 -x793 x794 -x795 x796 x797 -x798 -x799 x800 x801 -x802 -x803 x804 -x805 x806 x807 -x808 -x809 x810 -x811 x812 -x813 x814 x815 -x816 -x817 x818 x819 -x820 -x821 x822 -x823 x824 x825 -x826 -x827 x828 -x829 x830 x831 -x832 -x833 x834 -x835 x836 x837 -x838 -x839 x840 -x841 x842 -x843 x844 x845 -x846 -x847 x848 x849 -x850 -x851 x852 -x853 x854 -x855 x856 x857 -x858 -x859 x860 x861 -x862 -x863 x864 -x865 x866 x867 -x868 -x869 x870 -x871 x872 -x873 x874 x875 -x876 -x877 x878 x879 -x880 -x881 x882 -x883 x884 -x885 x886 x887 -x888 -x889 x890 x891 -x892 -x893 x894 -x895 x896 x897 -x898 -x899 x900 -x901 x902 -x903 x904 x905 -x906 -x907 x908 x909 -x910 -x911 x912 -x913 x914 -x915 x916 x917 -x918 -x919 x920 -x921 x922 x923 -x924 -x925 x926 x927 -x928 -x929 x930 -x931 x932 -x933 x934 x935 -x936 -x937 x938 -x939 x940 x941 -x942 -x943 x944 -x945 x946 x947 -x948 -x949 x950 -x951 x952 x953 -x954 -x955 x956 -x957 x958 x959 -x960 -x961 x962 x963 -x964 -x965 x966 -x967 x968 x969 -x970 -x971 x972 -x973 x974 -x975 x976 x977 -x978 -x979 x980 x981 -x982 -x983 x984 -x985 x986 -x987 x988 x989 -x990 -x991 x992 -x993 x994 x995 -x996 -x997 x998 -x999 x1000 x1001 -x1002 -x1003 x1004 x1005 -x1006 -x1007 x1008 -x1009 x1010 x1011 -x1012 -x1013 x1014 -x1015 x1016 x1017 -x1018 -x1019 x1020 -x1021 x1022 -x1023 x1024 x1025 -x1026 -x1027 x1028 -x1029 x1030 x1031 -x1032 -x1033 x1034 -x1035 x1036 x1037 -x1038 -x1039 x1040 x1041 -x1042 -x1043 x1044 c _______________________________________________________________________________ c c restarts : 23 c conflicts : 67464 (82 /sec) c decisions : 344664 (418 /sec) c propagations : 26472316 (32082 /sec) c inspects : 253785185 (307566 /sec) c CPU time : 825.141 s c _______________________________________________________________________________ #### 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): 1.15 1.03 0.94 2/54 32046 Raw data (stat): 32046 (runsolver) R 32045 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480177203 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.001 s] Raw data (loadavg): 1.12 1.03 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7071 0 0 0 971 27 0 0 25 0 1 0 480177203 32747520 6927 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7995 6927 603 41 0 7954 0 vsize: 31980 [startup+20.0008 s] Raw data (loadavg): 1.10 1.03 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7071 0 0 0 1972 27 0 0 25 0 1 0 480177203 32747520 6927 4294967295 134512640 134672761 3221224576 3221223024 134643987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7995 6927 603 41 0 7954 0 vsize: 31980 [startup+30.0012 s] Raw data (loadavg): 1.09 1.03 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7072 0 0 0 2972 27 0 0 25 0 1 0 480177203 32747520 6928 4294967295 134512640 134672761 3221224576 3221223024 134643556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7995 6928 603 41 0 7954 0 vsize: 31980 [startup+40.0015 s] Raw data (loadavg): 1.07 1.03 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7072 0 0 0 3971 27 0 0 25 0 1 0 480177203 32747520 6928 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7995 6928 603 41 0 7954 0 vsize: 31980 [startup+50.0021 s] Raw data (loadavg): 1.06 1.03 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7072 0 0 0 4971 27 0 0 25 0 1 0 480177203 32747520 6928 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7995 6928 603 41 0 7954 0 vsize: 31980 [startup+60.0026 s] Raw data (loadavg): 1.05 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7255 0 0 0 5955 43 0 0 25 0 1 0 480177203 33312768 7057 4294967295 134512640 134672761 3221224576 3221223024 134644032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8133 7057 603 41 0 8092 0 vsize: 32532 [startup+70.0027 s] Raw data (loadavg): 1.04 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7256 0 0 0 6951 48 0 0 25 0 1 0 480177203 33312768 7058 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8133 7058 603 41 0 8092 0 vsize: 32532 [startup+80.0035 s] Raw data (loadavg): 1.04 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7256 0 0 0 7949 50 0 0 25 0 1 0 480177203 33312768 7058 4294967295 134512640 134672761 3221224576 3221223024 134644040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8133 7058 603 41 0 8092 0 vsize: 32532 [startup+90.003 s] Raw data (loadavg): 1.03 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7257 0 0 0 8947 51 0 0 25 0 1 0 480177203 33312768 7059 4294967295 134512640 134672761 3221224576 3221223024 134644040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8133 7059 603 41 0 8092 0 vsize: 32532 [startup+100.003 s] Raw data (loadavg): 1.02 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7257 0 0 0 9947 51 0 0 25 0 1 0 480177203 33312768 7059 4294967295 134512640 134672761 3221224576 3221223024 134643959 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8133 7059 603 41 0 8092 0 vsize: 32532 [startup+110.004 s] Raw data (loadavg): 1.02 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7257 0 0 0 10947 51 0 0 25 0 1 0 480177203 33312768 7059 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8133 7059 603 41 0 8092 0 vsize: 32532 [startup+120.003 s] Raw data (loadavg): 1.02 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7257 0 0 0 11947 51 0 0 25 0 1 0 480177203 33312768 7059 4294967295 134512640 134672761 3221224576 3221223024 134643556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8133 7059 603 41 0 8092 0 vsize: 32532 [startup+130.003 s] Raw data (loadavg): 1.01 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7257 0 0 0 12947 52 0 0 25 0 1 0 480177203 33312768 7059 4294967295 134512640 134672761 3221224576 3221223024 134643565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8133 7059 603 41 0 8092 0 vsize: 32532 [startup+140.003 s] Raw data (loadavg): 1.01 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7257 0 0 0 13947 52 0 0 25 0 1 0 480177203 33050624 7014 4294967295 134512640 134672761 3221224576 3221222748 134642759 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8069 7014 603 41 0 8028 0 vsize: 32276 [startup+150.003 s] Raw data (loadavg): 1.01 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7257 0 0 0 14947 52 0 0 25 0 1 0 480177203 33050624 7014 4294967295 134512640 134672761 3221224576 3221222976 134605852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8069 7014 603 41 0 8028 0 vsize: 32276 [startup+160.003 s] Raw data (loadavg): 1.01 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7343 0 0 0 15947 52 0 0 25 0 1 0 480177203 33533952 7093 4294967295 134512640 134672761 3221224576 3221223120 134621211 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8187 7093 603 41 0 8146 0 vsize: 32748 [startup+170.002 s] Raw data (loadavg): 1.01 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 7343 0 0 0 16947 52 0 0 25 0 1 0 480177203 33050624 7015 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8069 7015 603 41 0 8028 0 vsize: 32276 [startup+180.003 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 8194 0 0 0 17945 54 0 0 25 0 1 0 480177203 36548608 7866 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 7866 603 41 0 8882 0 vsize: 35692 [startup+190.003 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 11824 0 0 0 18928 71 0 0 25 0 1 0 480177203 46800896 9745 4294967295 134512640 134672761 3221224576 3221223120 134621211 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11426 9745 603 41 0 11385 0 vsize: 45704 [startup+200.003 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12232 0 0 0 19920 78 0 0 25 0 1 0 480177203 47874048 9991 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11688 9991 603 41 0 11647 0 vsize: 46752 [startup+210.003 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12232 0 0 0 20921 78 0 0 25 0 1 0 480177203 47874048 9991 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11688 9991 603 41 0 11647 0 vsize: 46752 [startup+220.003 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12253 0 0 0 21920 78 0 0 25 0 1 0 480177203 47841280 9970 4294967295 134512640 134672761 3221224576 3221223024 134644008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11680 9970 603 41 0 11639 0 vsize: 46720 [startup+230.004 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12253 0 0 0 22920 78 0 0 25 0 1 0 480177203 47841280 9970 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11680 9970 603 41 0 11639 0 vsize: 46720 [startup+240.004 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12264 0 0 0 23913 85 0 0 25 0 1 0 480177203 47792128 9965 4294967295 134512640 134672761 3221224576 3221223024 134643524 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11668 9965 603 41 0 11627 0 vsize: 46672 [startup+250.004 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12264 0 0 0 24909 89 0 0 25 0 1 0 480177203 47788032 9965 4294967295 134512640 134672761 3221224576 3221223024 134644014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11667 9965 603 41 0 11626 0 vsize: 46668 [startup+260.005 s] Raw data (loadavg): 1.00 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12264 0 0 0 25908 90 0 0 25 0 1 0 480177203 47788032 9965 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11667 9965 603 41 0 11626 0 vsize: 46668 [startup+270.004 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12264 0 0 0 26906 91 0 0 25 0 1 0 480177203 47788032 9965 4294967295 134512640 134672761 3221224576 3221223056 134541817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11667 9965 603 41 0 11626 0 vsize: 46668 [startup+280.004 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12265 0 0 0 27906 92 0 0 25 0 1 0 480177203 47951872 9966 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11707 9966 603 41 0 11666 0 vsize: 46828 [startup+290.005 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12265 0 0 0 28906 92 0 0 25 0 1 0 480177203 47951872 9966 4294967295 134512640 134672761 3221224576 3221223024 134643499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11707 9966 603 41 0 11666 0 vsize: 46828 [startup+300.004 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12265 0 0 0 29906 92 0 0 25 0 1 0 480177203 47689728 9924 4294967295 134512640 134672761 3221224576 3221223120 134621211 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11643 9924 603 41 0 11602 0 vsize: 46572 [startup+310.005 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 12340 0 0 0 30906 92 0 0 25 0 1 0 480177203 47689728 9951 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11643 9951 603 41 0 11602 0 vsize: 46572 [startup+320.005 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 13955 0 0 0 31901 96 0 0 25 0 1 0 480177203 54304768 11566 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13258 11566 603 41 0 13217 0 vsize: 53032 [startup+330.006 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 15767 0 0 0 32898 100 0 0 25 0 1 0 480177203 61743104 13378 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15074 13378 603 41 0 15033 0 vsize: 60296 [startup+340.006 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 17441 0 0 0 33894 104 0 0 25 0 1 0 480177203 68640768 15052 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16758 15052 603 41 0 16717 0 vsize: 67032 [startup+350.006 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 19362 0 0 0 34889 108 0 0 25 0 1 0 480177203 76554240 16973 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18690 16973 603 41 0 18649 0 vsize: 74760 [startup+360.006 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 21241 0 0 0 35886 112 0 0 25 0 1 0 480177203 84189184 18852 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20554 18852 603 41 0 20513 0 vsize: 82216 [startup+370.006 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 23340 0 0 0 36881 116 0 0 25 0 1 0 480177203 92852224 20951 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22669 20951 603 41 0 22628 0 vsize: 90676 [startup+380.007 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 25458 0 0 0 37878 120 0 0 25 0 1 0 480177203 101441536 23069 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24766 23069 603 41 0 24725 0 vsize: 99064 [startup+390.007 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 26887 0 0 0 38875 123 0 0 25 0 1 0 480177203 107278336 24498 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26191 24498 603 41 0 26150 0 vsize: 104764 [startup+400.008 s] Raw data (loadavg): 1.07 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 28506 0 0 0 39872 126 0 0 25 0 1 0 480177203 114028544 26117 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27839 26117 603 41 0 27798 0 vsize: 111356 [startup+410.008 s] Raw data (loadavg): 1.06 1.02 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 29787 0 0 0 40869 130 0 0 25 0 1 0 480177203 119296000 27398 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29125 27398 603 41 0 29084 0 vsize: 116500 [startup+420.008 s] Raw data (loadavg): 1.05 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 30730 0 0 0 41868 131 0 0 25 0 1 0 480177203 123174912 28341 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30072 28341 603 41 0 30031 0 vsize: 120288 [startup+430.009 s] Raw data (loadavg): 1.04 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 32012 0 0 0 42865 134 0 0 25 0 1 0 480177203 128434176 29623 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31356 29623 603 41 0 31315 0 vsize: 125424 [startup+440.009 s] Raw data (loadavg): 1.04 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 33861 0 0 0 43861 138 0 0 25 0 1 0 480177203 136007680 31472 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33205 31472 603 41 0 33164 0 vsize: 132820 [startup+450.008 s] Raw data (loadavg): 1.03 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 35591 0 0 0 44856 143 0 0 25 0 1 0 480177203 143007744 33202 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34914 33202 603 41 0 34873 0 vsize: 139656 [startup+460.009 s] Raw data (loadavg): 1.02 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 37619 0 0 0 45852 147 0 0 25 0 1 0 480177203 151355392 35230 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36952 35230 603 41 0 36911 0 vsize: 147808 [startup+470.009 s] Raw data (loadavg): 1.02 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 39608 0 0 0 46849 151 0 0 25 0 1 0 480177203 159498240 37219 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38940 37219 603 41 0 38899 0 vsize: 155760 [startup+480.01 s] Raw data (loadavg): 1.02 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 41544 0 0 0 47845 155 0 0 25 0 1 0 480177203 167481344 39155 4294967295 134512640 134672761 3221224576 3221223680 134604309 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40889 39155 603 41 0 40848 0 vsize: 163556 [startup+490.01 s] Raw data (loadavg): 1.01 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 42706 0 0 0 48843 157 0 0 25 0 1 0 480177203 172208128 40317 4294967295 134512640 134672761 3221224576 3221223712 134614670 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 42043 40317 603 41 0 42002 0 vsize: 168172 [startup+500.009 s] Raw data (loadavg): 1.01 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 43962 0 0 0 49840 160 0 0 25 0 1 0 480177203 177246208 41573 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43273 41573 603 41 0 43232 0 vsize: 173092 [startup+510.009 s] Raw data (loadavg): 1.01 1.01 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 45140 0 0 0 50838 162 0 0 25 0 1 0 480177203 182161408 42751 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 44473 42751 603 41 0 44432 0 vsize: 177892 [startup+520.009 s] Raw data (loadavg): 1.01 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 46624 0 0 0 51835 166 0 0 25 0 1 0 480177203 188227584 44235 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 45954 44235 603 41 0 45913 0 vsize: 183816 [startup+530.01 s] Raw data (loadavg): 1.01 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 48170 0 0 0 52831 170 0 0 25 0 1 0 480177203 194514944 45781 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 47489 45781 603 41 0 47448 0 vsize: 189956 [startup+540.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 49394 0 0 0 53829 172 0 0 25 0 1 0 480177203 199618560 47005 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 48735 47005 603 41 0 48694 0 vsize: 194940 [startup+550.009 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 51324 0 0 0 54827 175 0 0 25 0 1 0 480177203 207589376 48935 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 50681 48935 603 41 0 50640 0 vsize: 202724 [startup+560.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 52582 0 0 0 55824 177 0 0 25 0 1 0 480177203 212754432 50193 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 51942 50193 603 41 0 51901 0 vsize: 207768 [startup+570.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 53472 0 0 0 56823 178 0 0 25 0 1 0 480177203 216379392 51083 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 52827 51083 603 41 0 52786 0 vsize: 211308 [startup+580.011 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 55424 0 0 0 57820 182 0 0 25 0 1 0 480177203 224370688 53035 4294967295 134512640 134672761 3221224576 3221223616 134614258 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 54778 53035 603 41 0 54737 0 vsize: 219112 [startup+590.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 57232 0 0 0 58815 187 0 0 25 0 1 0 480177203 231755776 54843 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 56581 54843 603 41 0 56540 0 vsize: 226324 [startup+600.01 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58137 0 0 0 59813 189 0 0 25 0 1 0 480177203 235450368 55748 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57483 55748 603 41 0 57442 0 vsize: 229932 [startup+610.011 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58263 0 0 0 60813 189 0 0 25 0 1 0 480177203 235876352 55865 4294967295 134512640 134672761 3221224576 3221223760 134615505 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55865 603 41 0 57546 0 vsize: 230348 [startup+620.011 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58263 0 0 0 61813 189 0 0 25 0 1 0 480177203 235876352 55865 4294967295 134512640 134672761 3221224576 3221223760 134615752 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55865 603 41 0 57546 0 vsize: 230348 [startup+630.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58263 0 0 0 62814 189 0 0 25 0 1 0 480177203 235876352 55865 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55865 603 41 0 57546 0 vsize: 230348 [startup+640.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58263 0 0 0 63814 189 0 0 25 0 1 0 480177203 235876352 55865 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55865 603 41 0 57546 0 vsize: 230348 [startup+650.012 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58263 0 0 0 64814 189 0 0 25 0 1 0 480177203 235876352 55865 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55865 603 41 0 57546 0 vsize: 230348 [startup+660.013 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58263 0 0 0 65814 189 0 0 25 0 1 0 480177203 235876352 55865 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55865 603 41 0 57546 0 vsize: 230348 [startup+670.014 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58264 0 0 0 66814 189 0 0 25 0 1 0 480177203 235876352 55866 4294967295 134512640 134672761 3221224576 3221223616 134613116 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55866 603 41 0 57546 0 vsize: 230348 [startup+680.014 s] Raw data (loadavg): 1.00 1.00 0.94 3/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58264 0 0 0 67815 189 0 0 25 0 1 0 480177203 235876352 55866 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55866 603 41 0 57546 0 vsize: 230348 [startup+690.014 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58264 0 0 0 68815 189 0 0 25 0 1 0 480177203 235876352 55866 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55866 603 41 0 57546 0 vsize: 230348 [startup+700.014 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58264 0 0 0 69815 189 0 0 25 0 1 0 480177203 235876352 55866 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55866 603 41 0 57546 0 vsize: 230348 [startup+710.015 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58264 0 0 0 70815 189 0 0 25 0 1 0 480177203 235876352 55866 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55866 603 41 0 57546 0 vsize: 230348 [startup+720.015 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58264 0 0 0 71815 189 0 0 25 0 1 0 480177203 235876352 55866 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55866 603 41 0 57546 0 vsize: 230348 [startup+730.015 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58265 0 0 0 72816 189 0 0 25 0 1 0 480177203 235876352 55867 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55867 603 41 0 57546 0 vsize: 230348 [startup+740.016 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58265 0 0 0 73816 189 0 0 25 0 1 0 480177203 235876352 55867 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55867 603 41 0 57546 0 vsize: 230348 [startup+750.016 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58265 0 0 0 74816 189 0 0 25 0 1 0 480177203 235876352 55867 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55867 603 41 0 57546 0 vsize: 230348 [startup+760.017 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58265 0 0 0 75816 189 0 0 25 0 1 0 480177203 235876352 55867 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55867 603 41 0 57546 0 vsize: 230348 [startup+770.017 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58265 0 0 0 76816 189 0 0 25 0 1 0 480177203 235876352 55867 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55867 603 41 0 57546 0 vsize: 230348 [startup+780.017 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58265 0 0 0 77817 189 0 0 25 0 1 0 480177203 235876352 55867 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55867 603 41 0 57546 0 vsize: 230348 [startup+790.017 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58265 0 0 0 78817 189 0 0 25 0 1 0 480177203 235876352 55867 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57587 55867 603 41 0 57546 0 vsize: 230348 [startup+800.017 s] Raw data (loadavg): 1.00 1.00 0.94 3/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 58675 0 0 0 79816 191 0 0 25 0 1 0 480177203 237563904 56277 4294967295 134512640 134672761 3221224576 3221223728 134565083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57999 56277 603 41 0 57958 0 vsize: 231996 [startup+810.018 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 60591 0 0 0 80812 195 0 0 25 0 1 0 480177203 245522432 58193 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 59942 58193 603 41 0 59901 0 vsize: 239768 [startup+820.018 s] Raw data (loadavg): 1.00 1.00 0.94 2/54 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 61798 0 0 0 81809 197 0 0 25 0 1 0 480177203 250458112 59400 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 61147 59400 603 41 0 61106 0 vsize: 244588 [startup+827.218 s] Raw data (loadavg): 1.00 1.00 0.94 1/53 32046 Raw data (stat): 32046 (minisat+) R 32045 27222 27221 0 -1 0 61798 0 0 0 81809 197 0 0 25 0 1 0 480177203 250458112 59400 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 61147 59400 603 41 0 61106 0 vsize: 0 Child status: 30 Real time (s): 827.218 CPU time (s): 827.273 CPU user time (s): 825.158 CPU system time (s): 2.11568 CPU usage (%): 100.007 Max. virtual memory (Kb): 244588 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 503 #### END VERIFIER DATA ####