HEAD is now at 5df24db initial deployement # Checking available version of Java # Java(TM) SE Runtime Environment (build 1.6.0_20-b02) # Running really p2cudf #Solver launched on Mon Jul 05 19:58:57 UTC 2010 #Using input file /home/misc2010/data/2010/impossible/rand835640.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-paranoid-1.6/rand835640.cudf.impossible.result #Objective function paranoid #Timeout 280s #java.runtime.name Java(TM) SE Runtime Environment #java.vm.name Java HotSpot(TM) Server VM #java.vm.version 16.3-b01 #java.vm.vendor Sun Microsystems Inc. #sun.arch.data.model 32 #java.version 1.6.0_20 #os.name Linux #os.version 2.6.18-6-xen-amd64 #os.arch i386 #Free memory 699792080 #Max memory 703463424 #Total memory 703463424 #Number of processors 2 #Parsing ... #Time to parse:3176 #Parsing done (3.177s). #Solving ... #Request size: 801 #Number of packages after slice: 15623 #Slice efficiency: 86% ## Optimization to Pseudo Boolean adapter # Pseudo Boolean Optimization # --- Begin Solver configuration --- # Stops conflict analysis at the first Unique Implication Point # org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure@7b6889 # Learn all clauses as in MiniSAT # claDecay=0.999 varDecay=0.95 conflictBoundIncFactor=1.5 initConflictBound=100 # VSIDS like heuristics from MiniSAT using a heap lightweight component caching from RSAT taking into account the objective function # Expensive reason simplification # Armin Biere (Picosat) restarts strategy # Glucose learned constraints deletion strategy # timeout=280s # DB Simplification allowed=false # --- End Solver configuration --- # Optimization function: misc 2010 paranoid # p cnf 28421 155159 # Current objective function value: 318206(1.16s) # Current objective function value: 289321(1.791s) # Current objective function value: 284467(2.028s) # Current objective function value: 197698(2.213s) # Current objective function value: 178428(2.364s) # Current objective function value: 178425(2.514s) # Current objective function value: 178424(2.798s) # Current objective function value: 178423(3.03s) # Paranoid criteria value: -37, -120 # Proof: [AbstractVariable: base-config, AbstractVariable: capplets, AbstractVariable: capplets-data, AbstractVariable: g++-2.95, AbstractVariable: gcc-2.95, AbstractVariable: gconf2, AbstractVariable: gnome-control-center, AbstractVariable: gnome-panel, AbstractVariable: gnome-panel-data, AbstractVariable: gnome-session, AbstractVariable: gnome-terminal, AbstractVariable: kile, AbstractVariable: libbonoboui2-0, AbstractVariable: libdigest-hmac-perl, AbstractVariable: libecal6, AbstractVariable: libedataserver3, AbstractVariable: libeel2-2, AbstractVariable: libgnome-desktop-2, AbstractVariable: libgnome2-0, AbstractVariable: libgnome2-common, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomevfs2-0, AbstractVariable: libgnomevfs2-common, AbstractVariable: libmail-spf-query-perl, AbstractVariable: libmyspell3, AbstractVariable: libnautilus2-2, AbstractVariable: libnet-dns-perl, AbstractVariable: libpanel-applet2-0, AbstractVariable: libstdc++2.10-dev, AbstractVariable: linux-kernel-headers, AbstractVariable: metacity, AbstractVariable: nautilus, AbstractVariable: openoffice.org, AbstractVariable: openoffice.org-bin, AbstractVariable: openoffice.org-debian-files, AbstractVariable: razor, AbstractVariable: xpdf-utils, AbstractVariable: aptitude-doc-ja, AbstractVariable: aspell-is, AbstractVariable: base-config, AbstractVariable: binutils, AbstractVariable: capplets, AbstractVariable: capplets-data, AbstractVariable: fftw2, AbstractVariable: fontconfig, AbstractVariable: fontconfig-config, AbstractVariable: g++-2.95, AbstractVariable: gcc-2.95, AbstractVariable: gcc-4.4-base, AbstractVariable: gconf2, AbstractVariable: gconf2-common, AbstractVariable: gnome-control-center, AbstractVariable: gnome-panel, AbstractVariable: gnome-panel-data, AbstractVariable: gnome-session, AbstractVariable: gnome-terminal, AbstractVariable: guile-1.6-libs, AbstractVariable: kile, AbstractVariable: libatlas3gf-amd64sse3, AbstractVariable: libblas-dev, AbstractVariable: libblas3gf, AbstractVariable: libbonoboui2-0, AbstractVariable: libc-bin, AbstractVariable: libc-dev-bin, AbstractVariable: libc6, AbstractVariable: libc6-dev, AbstractVariable: libcairo2, AbstractVariable: libcairo2-dev, AbstractVariable: libctl3, AbstractVariable: libdigest-hmac-perl, AbstractVariable: libecal6, AbstractVariable: libedataserver3, AbstractVariable: libeel2-2, AbstractVariable: libfontconfig1, AbstractVariable: libfontconfig1-dev, AbstractVariable: libfreetype6, AbstractVariable: libfreetype6-dev, AbstractVariable: libgcc1, AbstractVariable: libgconf2-4, AbstractVariable: libgcrypt11, AbstractVariable: libgdbm3, AbstractVariable: libgfortran3, AbstractVariable: libglib2.0-0, AbstractVariable: libglib2.0-data, AbstractVariable: libglib2.0-dev, AbstractVariable: libgnome-desktop-2, AbstractVariable: libgnome2-0, AbstractVariable: libgnome2-common, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomevfs2-0, AbstractVariable: libgnomevfs2-common, AbstractVariable: libgpg-error0, AbstractVariable: libguile-ltdl-1, AbstractVariable: libhdf5-serial-1.6.6-0, AbstractVariable: libice6, AbstractVariable: libkdecore5, AbstractVariable: libkdeui5, AbstractVariable: libkscreensaver5, AbstractVariable: libltt-0.9, AbstractVariable: liblzma2, AbstractVariable: libmail-spf-query-perl, AbstractVariable: libmng1, AbstractVariable: libmyspell3, AbstractVariable: libnautilus2-2, AbstractVariable: libnet-dns-perl, AbstractVariable: libnucleus5, AbstractVariable: liborbit2, AbstractVariable: libpanel-applet2-0, AbstractVariable: libpango1.0-0, AbstractVariable: libpango1.0-common, AbstractVariable: libpango1.0-dev, AbstractVariable: libpng12-0, AbstractVariable: libpng12-dev, AbstractVariable: libpoppler3, AbstractVariable: libqt4-dbus, AbstractVariable: libqt4-network, AbstractVariable: libqt4-svg, AbstractVariable: libqt4-xml, AbstractVariable: libqtcore4, AbstractVariable: libqtgui4, AbstractVariable: libqthreads-12, AbstractVariable: libruby1.6, AbstractVariable: libstdc++2.10-dev, AbstractVariable: libstdc++6, AbstractVariable: libtool, AbstractVariable: libxfixes3, AbstractVariable: libxml2, AbstractVariable: libxrender-dev, AbstractVariable: libxrender1, AbstractVariable: libxslt1.1, AbstractVariable: libzip-ruby1.6, AbstractVariable: libzlib-ruby1.6, AbstractVariable: linux-kernel-headers, AbstractVariable: linux-libc-dev, AbstractVariable: locales, AbstractVariable: lsb-base, AbstractVariable: ltt, AbstractVariable: ltt-tracer, AbstractVariable: ltt-visualizer, AbstractVariable: metacity, AbstractVariable: mpb, AbstractVariable: nautilus, AbstractVariable: openoffice.org, AbstractVariable: openoffice.org-bin, AbstractVariable: openoffice.org-debian-files, AbstractVariable: php4-ldap, AbstractVariable: phpldapadmin, AbstractVariable: poppler-utils, AbstractVariable: python-rpy-doc, AbstractVariable: razor, AbstractVariable: render-dev, AbstractVariable: rpl, AbstractVariable: ssh, AbstractVariable: vdr-dev, AbstractVariable: x11-common, AbstractVariable: xfree86-common, AbstractVariable: xpdf-utils] # starts : 13 # conflicts : 1296 # decisions : 267194 # propagations : 8703077 # inspects : 28751739 # learnt literals : 53 # learnt binary clauses : 202 # learnt ternary clauses : 136 # learnt clauses : 1242 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 4634 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 0 # number of reductions to clauses (during analyze) : 0 # number of learned constraints concerned by reduction : 0 # number of learning phase by resolution : 0 # number of learning phase by cutting planes : 0 # speed (assignments/second) : 2387675.4458161867 # non guided choices 58919 # learnt constraints type #Solving done (9.512s). #Solution contains:744