$ treengeling mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf c Treengeling Cube and Conquer SAT Solver c c Version ats 57807c8f410a9e676816984a0ad0c410e485bcae c c Copyright (C) 2010-2013 Armin Biere JKU Linz Austria. c All rights reserved. c c released Wed Oct 16 17:03:36 CEST 2013 c compiled Mo 11. Nov 13:07:51 CET 2013 c c gcc (Ubuntu/Linaro 4.8.1-10ubuntu8) 4.8.1 c -Wall -O3 -DNDBLSCR -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLPICOSAT c Linux sheckley 3.11.0-13-generic x86_64 c c verbose level 0 c will NOT print statistics for each solver instance c will print satisfying assignment c c splitting small nodes first (no '-b' option) c asymmetric splitting ('--asymmetric') c full search/simplification round interval 10 c no randomization in lookahead c c 'sysconf' reports 8 processors online c found 4 unique core ids in '/proc/cpuinfo' c found 1 unique physical ids in '/proc/cpuinfo' c 4 cores = 4 core times 1 physical ids in '/proc/cpuinfo' c found Intel as vendor in '/proc/cpuinfo' c 'sysconf' result off by a factor of 2.000000 on Intel c trusting 'sysconf' on Intel (assuming HyperThreading) c c maximum 8 workers (no '-t ' option) c using one worker for additional solver instance c maximum of 56 active nodes (no '-a ' option) c c 16416924 KB total memory according to '/proc/meminfo' c hard memory limit of 16032 MB (no '-g' nor '-m' option) c soft memory limit of 5344 MB c c default minimum conflict limit of 1000 conflicts c default initial conflict limit of 10000 conflicts c default maximum conflict limit of 100000 conflicts c c reading mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf c found 'p cnf 696 2320' header c parsed 4872 literals in 2320 clauses c cloning and starting additional solver instances c [0 1] 0.0 sec, 0 MB, 1 nodes +1 -0, vars 696 696 696, limit 10000 c (1 2) 1.3 sec, 4 MB, 2 nodes +2 -0, vars 458 463 463, limit 10000 c (2 4) 2.6 sec, 7 MB, 4 nodes +2 -0, vars 447 459 459, limit 5000 c (3 8) 3.7 sec, 6 MB, 8 nodes +4 -0, vars 436 449 449, limit 2500 c (4 16) 5.9 sec, 11 MB, 16 nodes +8 -0, vars 427 446 446, limit 1250 c (5 32) 9.1 sec, 19 MB, 32 nodes +16 -0, vars 401 440 440, limit 1000 c (6 60) 13.5 sec, 35 MB, 60 nodes +28 -0, vars 398 420 433, limit 1000 c (7 88) 18.0 sec, 53 MB, 88 nodes +28 -0, vars 391 407 433, limit 1000 c (8 116) 22.7 sec, 52 MB, 116 nodes +27 -0, vars 371 391 433, limit 1000 c (9 144) 27.2 sec, 71 MB, 144 nodes +28 -0, vars 361 383 433, limit 1000 c [10 172] 32.1 sec, 74 MB, 172 nodes +28 -0, vars 357 369 430, limit 1000 c (11 200) 37.0 sec, 95 MB, 200 nodes +28 -0, vars 353 361 430, limit 1000 c (12 228) 41.6 sec, 108 MB, 228 nodes +28 -0, vars 338 353 430, limit 1000 c (13 256) 46.3 sec, 115 MB, 256 nodes +27 -0, vars 316 336 430, limit 1000 c (14 284) 50.8 sec, 135 MB, 284 nodes +28 -0, vars 316 325 430, limit 1000 c (15 312) 55.3 sec, 146 MB, 312 nodes +28 -0, vars 309 319 430, limit 1000 c (16 340) 59.9 sec, 169 MB, 340 nodes +28 -0, vars 308 314 430, limit 1000 c (17 368) 64.7 sec, 177 MB, 368 nodes +26 -0, vars 283 295 430, limit 1000 c (18 396) 69.2 sec, 191 MB, 396 nodes +28 -0, vars 279 285 430, limit 1000 c (19 424) 73.8 sec, 202 MB, 424 nodes +28 -0, vars 266 272 430, limit 1000 c [20 452] 78.6 sec, 200 MB, 452 nodes +27 -0, vars 262 267 430, limit 1000 c (21 480) 83.6 sec, 217 MB, 480 nodes +28 -0, vars 250 261 430, limit 1000 c (22 508) 88.3 sec, 220 MB, 508 nodes +28 -0, vars 223 238 430, limit 1000 c (23 536) 92.8 sec, 232 MB, 536 nodes +28 -0, vars 223 231 430, limit 1000 c (24 564) 97.3 sec, 236 MB, 564 nodes +27 -0, vars 208 224 430, limit 1000 c (25 590) 101.8 sec, 248 MB, 588 nodes +26 -2, vars 188 217 430, limit 1000 c (26 611) 105.4 sec, 249 MB, 602 nodes +19 -7, vars 140 206 430, limit 1000 c (27 624) 107.7 sec, 249 MB, 600 nodes +13 -15, vars 139 201 430, limit 1000 c (28 624) 108.4 sec, 233 MB, 568 nodes +0 -32, vars 122 218 430, limit 2000 c (29 624) 109.1 sec, 223 MB, 528 nodes +0 -40, vars 137 229 430, limit 2788 c [30 639] 113.7 sec, 218 MB, 530 nodes +15 -13, vars 182 223 430, limit 3028 c (31 655) 119.0 sec, 220 MB, 534 nodes +15 -12, vars 136 219 430, limit 2725 c (32 666) 122.1 sec, 212 MB, 528 nodes +11 -17, vars 117 213 430, limit 2453 c (33 666) 123.2 sec, 197 MB, 480 nodes +0 -48, vars 115 239 430, limit 4906 c (34 678) 126.8 sec, 197 MB, 476 nodes +12 -16, vars 134 255 430, limit 3920 c (35 695) 133.1 sec, 200 MB, 482 nodes +17 -11, vars 198 239 430, limit 7840 c (36 719) 140.3 sec, 213 MB, 502 nodes +24 -4, vars 193 233 430, limit 7056 c (37 725) 144.1 sec, 202 MB, 486 nodes +6 -22, vars 69 230 430, limit 6350 c (38 725) 147.8 sec, 184 MB, 446 nodes +0 -40, vars 196 263 430, limit 12700 c (39 733) 154.7 sec, 179 MB, 434 nodes +8 -20, vars 198 268 430, limit 13250 c [40 742] 166.0 sec, 182 MB, 424 nodes +9 -19, vars 72 269 430, limit 26500 c (41 742) 209.9 sec, 197 MB, 392 nodes +0 -32, vars 200 279 430, limit 53000 c (42 742) 239.7 sec, 169 MB, 347 nodes +0 -45, vars 246 286 430, limit 100000 c (43 758) 290.9 sec, 186 MB, 351 nodes +16 -12, vars 251 289 430, limit 100000 c (44 780) 343.5 sec, 208 MB, 367 nodes +22 -6, vars 116 282 430, limit 90000 c (45 780) 376.2 sec, 167 MB, 334 nodes +0 -33, vars 123 300 430, limit 81000 c (46 787) 428.1 sec, 165 MB, 320 nodes +7 -21, vars 223 311 430, limit 100000 c (47 798) 481.1 sec, 163 MB, 314 nodes +11 -17, vars 115 309 430, limit 100000 c (48 817) 539.0 sec, 180 MB, 324 nodes +19 -9, vars 111 298 430, limit 100000 **INTERRUPTED**