$ lingeling mod2-3cage-unsat-9-10-vertex-cover-with-conflicts.cnf c Lingeling 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 reading input file mod2-3cage-unsat-9-10-vertex-cover-with-conflicts.cnf c no embedded options c found 'p cnf 696 6688' header c read 696 variables, 6688 clauses, 13608 literals in 0.0 seconds c c seconds irredundant redundant clauses agility height c variables clauses conflicts large ternary binary glue MB c c S 0.0 696 6688 0 0 0 0 0 0.0 0.0 0 c P 1.0 86 429 76200 4727 62 18 37 13.3 16.5 1 c S 2.1 86 429 163102 10221 62 18 39 13.4 16.2 2 c S 5.0 86 429 393612 6494 64 18 41 12.9 15.6 2 c S 10.1 86 429 706587 15184 64 18 33 12.9 15.1 4 c S 20.0 86 429 1355971 15060 64 18 37 12.4 14.8 3 c S 30.0 86 429 1965126 13407 64 18 36 12.1 14.4 3 c S 40.0 86 429 2501181 25728 65 18 33 11.8 13.9 6 c S 50.0 86 429 2954571 38851 83 19 35 11.5 13.6 7 c S 60.2 86 429 3361551 30483 83 19 33 11.4 13.5 5 c S 120.1 81 428 6037555 22974 397 54 36 10.6 12.7 3 c c seconds irredundant redundant clauses agility height c variables clauses conflicts large ternary binary glue MB c s UNSATISFIABLE c c 1.094 1% simplifying c 124.314 99% search c ================================== c 125.408 100% all c c 8647016 decisions, 68950.9 decisions/sec c 6318208 conflicts, 50381.1 conflicts/sec c 64251290 propagations, 0.5 megaprops/sec c 125.4 seconds, 16.3 MB