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 Tue Jul 06 01:36:39 UTC 2010 #Using input file /home/misc2010/data/2010/difficult/randf61f65.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-paranoid-1.6/randf61f65.cudf.difficult.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:1497 #Parsing done (1.498s). #Solving ... #Request size: 744 #Number of packages after slice: 5470 #Slice efficiency: 90% ## 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@64f6cd # 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 11913 48355 # Current objective function value: 103780(0.741s) # Current objective function value: 103772(1.11s) # Current objective function value: 88525(1.211s) # Current objective function value: 79439(1.456s) # Current objective function value: 73304(1.59s) # Current objective function value: 70393(1.834s) # Current objective function value: 70349(1.976s) # Current objective function value: 70326(2.1s) # Current objective function value: 55152(2.184s) # Current objective function value: 55148(2.944s) # Current objective function value: 52146(3.033s) # Current objective function value: 49129(3.093s) # Current objective function value: 49119(3.158s) # Current objective function value: 49104(3.238s) # Current objective function value: 49089(3.437s) # Current objective function value: 49083(3.998s) # Current objective function value: 49082(4.638s) # Current objective function value: 49079(5.186s) # Current objective function value: 49077(6.816s) # cleaning 2466 clauses out of 4937 with flag 5000/5000 # Current objective function value: 49076(8.801s) # Current objective function value: 49075(10.511s) # cleaning 4231 clauses out of 8471 with flag 11000/11000 # cleaning 5620 clauses out of 11239 with flag 18000/18000 # cleaning 6807 clauses out of 13620 with flag 26001/26001 # Current objective function value: 49074(29.628s) # cleaning 7904 clauses out of 15811 with flag 35000/35000 # Current objective function value: 49073(35.203s) # cleaning 8941 clauses out of 17907 with flag 45000/45000 # cleaning 9972 clauses out of 19968 with flag 56002/56002 # cleaning 10995 clauses out of 21994 with flag 68000/68000 # cleaning 11991 clauses out of 23999 with flag 81000/81000 # cleaning 12982 clauses out of 26008 with flag 95000/95000 # cleaning 14000 clauses out of 28026 with flag 110000/110000 # Current objective function value: 49072(126.256s) # cleaning 15007 clauses out of 30027 with flag 126002/126002 # cleaning 15997 clauses out of 32018 with flag 143001/143001 # cleaning 17005 clauses out of 34021 with flag 161001/161001 # cleaning 18004 clauses out of 36015 with flag 180000/180000 # cleaning 18990 clauses out of 38011 with flag 200000/200000 # cleaning 20002 clauses out of 40022 with flag 221001/221001 # cleaning 21010 clauses out of 42019 with flag 243000/243000 # cleaning 22002 clauses out of 44009 with flag 266001/266001 # Paranoid criteria value: -16, -320 # Proof: [AbstractVariable: antlr, AbstractVariable: apt-listchanges, AbstractVariable: aptitude, AbstractVariable: gcc-4.3, AbstractVariable: gforge-plugin-scmgit, AbstractVariable: libantlr-java, AbstractVariable: libantlr-java-gcj, AbstractVariable: libept0, AbstractVariable: myspell-ru, AbstractVariable: nagios2-common, AbstractVariable: nagios2-doc, AbstractVariable: qstat, AbstractVariable: snmp, AbstractVariable: tasksel, AbstractVariable: tasksel-data, AbstractVariable: uuid-runtime, AbstractVariable: amule-utils-gui, AbstractVariable: ant, AbstractVariable: ant-optional, AbstractVariable: antlr, AbstractVariable: apt-listchanges, AbstractVariable: aptitude, AbstractVariable: aspell, AbstractVariable: aspell-is, AbstractVariable: autodocktools, AbstractVariable: binutils, AbstractVariable: blt, AbstractVariable: bochsbios, AbstractVariable: cli-common, AbstractVariable: cpp, AbstractVariable: cpp-4.4, AbstractVariable: cwiid-dbg, AbstractVariable: dictionaries-common, AbstractVariable: g++-4.4, AbstractVariable: gamin, AbstractVariable: gcc, AbstractVariable: gcc-4.3, AbstractVariable: gcc-4.4, AbstractVariable: gcc-4.4-base, AbstractVariable: gconf2-common, AbstractVariable: gforge-plugin-scmgit, AbstractVariable: hicolor-icon-theme, AbstractVariable: hunspell-en-ca, AbstractVariable: install-info, AbstractVariable: java-wrappers, AbstractVariable: jeuclid-cli, AbstractVariable: kdelibs-data, AbstractVariable: kdelibs4c2a, AbstractVariable: libantlr-java, AbstractVariable: libantlr-java-gcj, AbstractVariable: libapache-session-perl, AbstractVariable: libapache2-mod-apreq2, AbstractVariable: libapache2-request-perl, AbstractVariable: libappconfig-perl, AbstractVariable: libapreq2, AbstractVariable: libart-2.0-2, AbstractVariable: libarts1c2a, AbstractVariable: libartsc0, AbstractVariable: libaspell15, AbstractVariable: libatlas3gf-core2sse3, AbstractVariable: libaudio-dev, AbstractVariable: libaudio2, AbstractVariable: libaudiofile0, AbstractVariable: libavahi-client3, AbstractVariable: libavahi-common-data, AbstractVariable: libavahi-common3, AbstractVariable: libavahi-glib1, AbstractVariable: libavahi-qt3-1, AbstractVariable: libavahi-ui0, AbstractVariable: libavahi-ui0.0-cil, AbstractVariable: libavahi1.0-cil, AbstractVariable: libavalon-framework-java, AbstractVariable: libavc1394-0, AbstractVariable: libbatik-java, AbstractVariable: libbluetooth3, AbstractVariable: libbonobo2-0, AbstractVariable: libbonobo2-common, AbstractVariable: libboost-iostreams1.40.0, AbstractVariable: libboost-regex1.40-dev, AbstractVariable: libboost-regex1.40.0, AbstractVariable: libboost1.40-dev, AbstractVariable: libbrlapi0.5, AbstractVariable: libbsf-java, AbstractVariable: libc-bin, AbstractVariable: libc-dev-bin, AbstractVariable: libc6, AbstractVariable: libc6-dev, AbstractVariable: libcairo-perl, AbstractVariable: libclassworlds-java, AbstractVariable: libcommons-cli-java, AbstractVariable: libcommons-lang-java, AbstractVariable: libcrypto++7, AbstractVariable: libcups2, AbstractVariable: libcups2-dev, AbstractVariable: libcupsdriver1, AbstractVariable: libcupsdriver1-dev, AbstractVariable: libcupsimage2, AbstractVariable: libcupsimage2-dev, AbstractVariable: libcwiid1, AbstractVariable: libdbus-1-3, AbstractVariable: libdrm2, AbstractVariable: libecj-java-gcj, AbstractVariable: libept0, AbstractVariable: libesd0, AbstractVariable: libexif12, AbstractVariable: libfile-tail-perl, AbstractVariable: libfontconfig1-dev, AbstractVariable: libfreebob0, AbstractVariable: libfreetype6, AbstractVariable: libfreetype6-dev, AbstractVariable: libgamin0, AbstractVariable: libgcc1, AbstractVariable: libgconf2-4, AbstractVariable: libgcrypt11, AbstractVariable: libgcrypt11-dev, AbstractVariable: libgdata1.2-1, AbstractVariable: libgdiplus, AbstractVariable: libgfortran3, AbstractVariable: libgl1-mesa-dev, AbstractVariable: libgl1-mesa-glx, AbstractVariable: libglade2-0, AbstractVariable: libglib-perl, AbstractVariable: libglib2.0-cil, AbstractVariable: libglu1-mesa, AbstractVariable: libglu1-mesa-dev, AbstractVariable: libgnome-menu2, AbstractVariable: libgnutls-dev, AbstractVariable: libgnutls26, AbstractVariable: libgomp1, AbstractVariable: libgpg-error-dev, AbstractVariable: libgpg-error0, AbstractVariable: libgssapi-krb5-2, AbstractVariable: libgstreamer-plugins-base0.10-0, AbstractVariable: libgstreamer0.10-0, AbstractVariable: libgtk2-gladexml-perl, AbstractVariable: libgtk2-perl, AbstractVariable: libgtk2.0-cil, AbstractVariable: libhunspell-1.2-0, AbstractVariable: libhyphen0, AbstractVariable: libice-dev, AbstractVariable: libicu-dev, AbstractVariable: libicu38, AbstractVariable: libicu42, AbstractVariable: libidl0, AbstractVariable: libiec61883-0, AbstractVariable: libjack0, AbstractVariable: libjeuclid-core-java, AbstractVariable: libjpeg62-dev, AbstractVariable: libk5crypto3, AbstractVariable: libkrb5-3, AbstractVariable: libkrb5support0, AbstractVariable: liblcms1, AbstractVariable: liblcms1-dev, AbstractVariable: liblog4cpp5, AbstractVariable: liblua50, AbstractVariable: liblualib50, AbstractVariable: libmad0, AbstractVariable: libmng-dev, AbstractVariable: libmng1, AbstractVariable: libmono-cairo1.0-cil, AbstractVariable: libmono-corlib1.0-cil, AbstractVariable: libmono-data-tds1.0-cil, AbstractVariable: libmono-security1.0-cil, AbstractVariable: libmono-sharpzip0.84-cil, AbstractVariable: libmono-system-data1.0-cil, AbstractVariable: libmono-system-web1.0-cil, AbstractVariable: libmono-system1.0-cil, AbstractVariable: libmono0, AbstractVariable: libmono1.0-cil, AbstractVariable: libmysqlclient16, AbstractVariable: libneon27, AbstractVariable: libnspr4-0d, AbstractVariable: libnss3-1d, AbstractVariable: libomniorb4-1, AbstractVariable: libomnithread3c2, AbstractVariable: liborbit2, AbstractVariable: libplexus-classworlds-java, AbstractVariable: libplexus-component-api-java, AbstractVariable: libplexus-container-default-java, AbstractVariable: libplexus-utils-java, AbstractVariable: libpng12-0, AbstractVariable: libpng12-dev, AbstractVariable: libpq5, AbstractVariable: libproc-daemon-perl, AbstractVariable: libpthread-stubs0, AbstractVariable: libpthread-stubs0-dev, AbstractVariable: libqt3-headers, AbstractVariable: libqt3-mt, AbstractVariable: libqt3-mt-dev, AbstractVariable: libqt4-dbus, AbstractVariable: libqt4-designer, AbstractVariable: libqt4-network, AbstractVariable: libqt4-qt3support, AbstractVariable: libqt4-script, AbstractVariable: libqt4-sql, AbstractVariable: libqt4-sql-sqlite, AbstractVariable: libqt4-xml, AbstractVariable: libqtcore4, AbstractVariable: libqtgui4, AbstractVariable: libsaml5, AbstractVariable: libscim8c2a, AbstractVariable: libshib-target5, AbstractVariable: libshib6, AbstractVariable: libsm-dev, AbstractVariable: libsoup2.4-1, AbstractVariable: libssl0.9.8, AbstractVariable: libstartup-notification0, AbstractVariable: libstdc++6, AbstractVariable: libstdc++6-4.4-dev, AbstractVariable: libstlport4.6ldbl, AbstractVariable: libsys-syslog-perl, AbstractVariable: libtasn1-3, AbstractVariable: libtasn1-3-dev, AbstractVariable: libtemplate-perl, AbstractVariable: libtiff4, AbstractVariable: libtiff4-dev, AbstractVariable: libtiffxx0c2, AbstractVariable: libvorbisfile3, AbstractVariable: libwnck-common, AbstractVariable: libwnck22, AbstractVariable: libwxbase2.8-0, AbstractVariable: libwxgtk2.8-0, AbstractVariable: libx11-dev, AbstractVariable: libxalan110, AbstractVariable: libxalan2-java, AbstractVariable: libxau-dev, AbstractVariable: libxaw7, AbstractVariable: libxcb-xlib0, AbstractVariable: libxcb-xlib0-dev, AbstractVariable: libxcb1, AbstractVariable: libxcb1-dev, AbstractVariable: libxcursor-dev, AbstractVariable: libxdelta2, AbstractVariable: libxdmcp-dev, AbstractVariable: libxerces-c28, AbstractVariable: libxext-dev, AbstractVariable: libxfixes-dev, AbstractVariable: libxft-dev, AbstractVariable: libxi-dev, AbstractVariable: libxinerama-dev, AbstractVariable: libxml-commons-external-java, AbstractVariable: libxml-libxml-common-perl, AbstractVariable: libxml-libxml-perl, AbstractVariable: libxml-namespacesupport-perl, AbstractVariable: libxml-sax-perl, AbstractVariable: libxml-security-c14, AbstractVariable: libxmlgraphics-commons-java, AbstractVariable: libxmu-dev, AbstractVariable: libxmu-headers, AbstractVariable: libxmu6, AbstractVariable: libxrandr-dev, AbstractVariable: libxrender-dev, AbstractVariable: libxres1, AbstractVariable: libxslt1.1, AbstractVariable: libxt-dev, AbstractVariable: libxtrap6, AbstractVariable: libxxf86misc1, AbstractVariable: libxxf86vm1, AbstractVariable: locales, AbstractVariable: lswm, AbstractVariable: mailgraph, AbstractVariable: menu-xdg, AbstractVariable: mesa-common-dev, AbstractVariable: mgltools-bhtree, AbstractVariable: mgltools-dejavu, AbstractVariable: mgltools-geomutils, AbstractVariable: mgltools-gle, AbstractVariable: mgltools-mglutil, AbstractVariable: mgltools-molkit, AbstractVariable: mgltools-opengltk, AbstractVariable: mgltools-pmv, AbstractVariable: mgltools-pybabel, AbstractVariable: mgltools-pyglf, AbstractVariable: mgltools-sff, AbstractVariable: mgltools-support, AbstractVariable: mgltools-viewerframework, AbstractVariable: mgltools-volume, AbstractVariable: mono-common, AbstractVariable: mono-gac, AbstractVariable: mono-jit, AbstractVariable: mono-runtime, AbstractVariable: myspell-ru, AbstractVariable: mysql-common, AbstractVariable: nagios-plugins-standard, AbstractVariable: nagios2-common, AbstractVariable: nagios2-doc, AbstractVariable: nscd, AbstractVariable: openbios-sparc, AbstractVariable: openhackware, AbstractVariable: openoffice.org-common, AbstractVariable: openoffice.org-core, AbstractVariable: openoffice.org-l10n-pl, AbstractVariable: openoffice.org-style-andromeda, AbstractVariable: oss-compat, AbstractVariable: procmail, AbstractVariable: procmail-lib, AbstractVariable: proll, AbstractVariable: python-central, AbstractVariable: python-cwiid, AbstractVariable: python-imaging, AbstractVariable: python-imaging-tk, AbstractVariable: python-numpy, AbstractVariable: python-pmw, AbstractVariable: python-tk, AbstractVariable: python-zsi, AbstractVariable: qemu, AbstractVariable: qstat, AbstractVariable: qt3-dev-tools, AbstractVariable: r-doc-pdf, AbstractVariable: scim, AbstractVariable: scim-thai, AbstractVariable: snmp, AbstractVariable: tasksel, AbstractVariable: tasksel-data, AbstractVariable: tcl8.4, AbstractVariable: tk8.4, AbstractVariable: torrus-common, AbstractVariable: ttf-opensymbol, AbstractVariable: uuid-runtime, AbstractVariable: vgabios, AbstractVariable: vym, AbstractVariable: wmgui, AbstractVariable: wminput, AbstractVariable: wterm, AbstractVariable: x11-xserver-utils, AbstractVariable: x11proto-core-dev, AbstractVariable: x11proto-fixes-dev, AbstractVariable: x11proto-input-dev, AbstractVariable: x11proto-kb-dev, AbstractVariable: x11proto-randr-dev, AbstractVariable: x11proto-render-dev, AbstractVariable: x11proto-xext-dev, AbstractVariable: x11proto-xinerama-dev, AbstractVariable: xsltproc, AbstractVariable: xtrans-dev, AbstractVariable: zip] # starts : 155 # conflicts : 277558 # decisions : 2512878 # propagations : 535315714 # inspects : 1243890578 # learnt literals : 68 # learnt binary clauses : 503 # learnt ternary clauses : 145 # learnt clauses : 277490 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 1677717 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 19 # 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) : 3474068.3241503285 # non guided choices 65284 # learnt constraints type #Solving done (282.433s). #Solution contains:921