$ lingeling mod2-3cage-unsat-9-10-vertex-cover-without-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-without-conflicts.cnf c no embedded options c found 'p cnf 696 2320' header c read 696 variables, 2320 clauses, 4872 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 2320 0 0 0 0 0 0.0 0.0 0 c S 1.0 464 1392 27799 4009 304 117 34 18.5 37.4 2 c P 2.0 464 1392 60204 5646 408 117 34 20.3 35.0 1 c P 5.0 464 1392 140205 10112 588 131 33 21.7 33.3 1 c S 10.0 464 1392 260130 18148 760 131 32 22.8 36.1 5 c S 20.1 464 1392 446840 29573 902 131 36 24.6 35.8 8 c S 30.0 464 1392 688412 17527 975 131 36 24.9 34.9 3 c S 40.0 464 1392 880593 29760 1023 131 34 25.1 34.2 8 c S 50.0 464 1392 1112193 24998 1073 131 35 25.1 33.6 6 c S 60.0 464 1392 1301436 31551 1099 131 34 25.1 33.1 6 c S 120.0 464 1392 2547965 10803 1194 131 35 24.9 31.7 2 c S 180.0 464 1392 3824238 44801 1313 131 33 23.9 30.4 16 c S 240.0 464 1392 4820001 44862 1389 131 35 22.8 29.9 12 c S 300.1 464 1392 5498966 78208 1471 131 33 22.7 29.9 20 c S 600.1 464 1392 8209890 77636 1568 131 30 22.6 29.7 31 c S 900.0 464 1392 13119364 49052 1725 131 33 22.0 28.6 17 c S 1800.1 464 1392 22958750 98750 1846 131 34 20.9 27.8 47 c S 2700.0 464 1392 29859729 232033 1865 131 33 20.6 28.1 85 c S 3600.1 464 1392 39400947 80448 1914 131 34 20.2 27.8 27 c S 4500.1 464 1392 49381455 66009 1967 131 34 20.2 27.8 24 c S 5400.1 464 1392 56661440 156566 1989 131 34 20.2 27.7 63 c S 6300.3 464 1392 61936487 211346 2010 131 33 20.3 27.6 44 c S 7200.1 464 1392 68721909 55905 2015 131 33 20.2 27.2 14 c c seconds irredundant redundant clauses agility height c variables clauses conflicts large ternary binary glue MB c c S 10800.1 464 1392 89996521 174065 2044 131 34 20.0 26.7 77 c S 14400.2 464 1392 104510218 378905 2059 131 34 20.1 26.5 99 c S 18000.3 464 1392 117971974 435974 2063 131 32 20.0 26.2 134 c S 21600.0 464 1392 130310650 383997 2065 131 34 20.1 26.2 115 c S 25200.1 464 1392 160551060 155962 2075 131 31 20.0 26.3 63 c S 28800.0 464 1392 192551073 95808 2076 131 31 19.9 26.2 28 c S 32400.1 464 1392 213821405 113555 2076 131 33 20.0 26.5 52 c S 36000.1 464 1392 229422256 242874 2076 131 32 20.0 26.5 96