$ lingeling mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.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-red-elim.cnf c no embedded options c found 'p cnf 348 1730' header c read 348 variables, 1730 clauses, 3576 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 348 1730 0 0 0 0 0 0.0 0.0 0 c S 1.0 83 460 78358 6726 9 19 42 12.9 18.6 2 c S 2.0 83 460 153973 11081 40 19 39 12.4 17.2 2 c S 5.0 83 460 384752 7623 40 19 42 12.0 15.9 2 c S 10.1 83 460 675499 20387 40 19 36 11.5 14.8 4 c S 20.0 83 460 1357728 15984 41 19 39 11.2 14.3 3 c S 30.0 83 460 1980260 12209 41 19 38 11.2 14.0 3 c S 40.1 83 460 2516346 35142 42 19 34 11.1 13.7 8 c S 50.0 83 460 2936082 25520 45 19 36 11.0 13.4 7 c S 60.1 83 460 3340377 47954 61 20 42 10.9 13.3 11 c S 120.0 78 460 6212673 18352 382 54 38 10.5 12.6 4 c c seconds irredundant redundant clauses agility height c variables clauses conflicts large ternary binary glue MB c s UNSATISFIABLE c c 1.268 1% simplifying c 131.464 99% search c ================================== c 132.732 100% all c c 9647858 decisions, 72686.7 decisions/sec c 6920638 conflicts, 52139.9 conflicts/sec c 66551218 propagations, 0.5 megaprops/sec c 132.7 seconds, 18.1 MB