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 22:40:29 UTC 2010 #Using input file /home/misc2010/data/2010/difficult/rand95e48b.cudf #Using ouput file /home/misc2010/tmp/201007051419/p2cudf-paranoid-1.6/rand95e48b.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:1383 #Parsing done (1.384s). #Solving ... #Request size: 746 #Number of packages after slice: 5308 #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 11643 47524 # Current objective function value: 222366(0.697s) # Current objective function value: 166102(1.19s) # Current objective function value: 130518(1.35s) # Current objective function value: 92054(1.445s) # Current objective function value: 89235(3.243s) # Current objective function value: 83207(3.292s) # cleaning 2457 clauses out of 4915 with flag 5001/5001 # cleaning 4229 clauses out of 8457 with flag 11000/11000 # cleaning 5609 clauses out of 11229 with flag 18001/18001 # cleaning 6806 clauses out of 13621 with flag 26002/26002 # cleaning 7904 clauses out of 15816 with flag 35003/35003 # cleaning 8950 clauses out of 17916 with flag 45007/45007 # cleaning 9975 clauses out of 19959 with flag 56000/56000 # cleaning 10983 clauses out of 21984 with flag 68000/68000 # cleaning 11993 clauses out of 24000 with flag 81000/81000 # cleaning 12994 clauses out of 26008 with flag 95001/95001 # cleaning 14002 clauses out of 28014 with flag 110001/110001 # cleaning 14991 clauses out of 30012 with flag 126001/126001 # cleaning 16007 clauses out of 32021 with flag 143001/143001 # cleaning 17001 clauses out of 34015 with flag 161002/161002 # cleaning 17994 clauses out of 36012 with flag 180000/180000 # cleaning 19000 clauses out of 38018 with flag 200000/200000 # cleaning 20003 clauses out of 40019 with flag 221001/221001 # cleaning 20998 clauses out of 42015 with flag 243000/243000 # cleaning 21995 clauses out of 44017 with flag 266000/266000 # cleaning 23004 clauses out of 46024 with flag 290002/290002 # cleaning 24006 clauses out of 48021 with flag 315003/315003 # cleaning 25000 clauses out of 50016 with flag 341004/341004 # cleaning 25998 clauses out of 52012 with flag 368000/368000 # Paranoid criteria value: -28, -327 # Proof: [AbstractVariable: ffmpeg, AbstractVariable: libapache-dbi-perl, AbstractVariable: libapache2-mod-perl2, AbstractVariable: libauthen-simple-ldap-perl, AbstractVariable: libgnutls13, AbstractVariable: libimlib2, AbstractVariable: libio-socket-ssl-perl, AbstractVariable: libldap2, AbstractVariable: liblzo-dev, AbstractVariable: liblzo1, AbstractVariable: libmysqlclient15off, AbstractVariable: libnet-ldap-perl, AbstractVariable: libwww-perl, AbstractVariable: mailx, AbstractVariable: mysql-client-5.0, AbstractVariable: netbase, AbstractVariable: nfs-common, AbstractVariable: nscd, AbstractVariable: ntpdate, AbstractVariable: php5-mhash, AbstractVariable: postfix, AbstractVariable: python-mysqldb, AbstractVariable: python-subversion, AbstractVariable: spamassassin, AbstractVariable: spampd, AbstractVariable: telnet, AbstractVariable: viewcvs, AbstractVariable: viewvc, AbstractVariable: ant-optional, AbstractVariable: ant-optional-gcj, AbstractVariable: apache2-mpm-prefork, AbstractVariable: apache2.2-bin, AbstractVariable: apache2.2-common, AbstractVariable: aptitude-doc-ja, AbstractVariable: aspell, AbstractVariable: aspell-is, AbstractVariable: avant-window-navigator, AbstractVariable: avant-window-navigator-data, AbstractVariable: awn-applets-python-extras, AbstractVariable: camlp4, AbstractVariable: camlp5, AbstractVariable: dbus, AbstractVariable: dbus-x11, AbstractVariable: dictionaries-common, AbstractVariable: ffmpeg, AbstractVariable: fontconfig-config, AbstractVariable: freetds-common, AbstractVariable: g++-4.3, AbstractVariable: g2ipmsg, AbstractVariable: gconf2, AbstractVariable: gconf2-common, AbstractVariable: ghc6, AbstractVariable: gimp, AbstractVariable: gimp-data, AbstractVariable: gimp-libcurl, AbstractVariable: gnome-control-center-dev, AbstractVariable: gnome-mime-data, AbstractVariable: gosa, AbstractVariable: hicolor-icon-theme, AbstractVariable: install-info, AbstractVariable: kanagram, AbstractVariable: kdeedu-data, AbstractVariable: kdelibs-data, AbstractVariable: kdelibs4c2a, AbstractVariable: libaa1, AbstractVariable: libapache-dbi-perl, AbstractVariable: libapache2-mod-perl2, AbstractVariable: libapache2-mod-php5, AbstractVariable: libapol4, AbstractVariable: libapr1, AbstractVariable: libaprutil1, AbstractVariable: libaprutil1-dbd-pgsql, AbstractVariable: libaprutil1-ldap, AbstractVariable: libart-2.0-2, AbstractVariable: libarts1c2a, AbstractVariable: libartsc0, AbstractVariable: libaspell15, AbstractVariable: libasyncns0, AbstractVariable: libatk1.0-0, AbstractVariable: libaudio2, AbstractVariable: libaudiofile0, AbstractVariable: libauthen-simple-ldap-perl, AbstractVariable: libauthen-simple-passwd-perl, AbstractVariable: libavahi-client3, AbstractVariable: libavahi-common-data, AbstractVariable: libavahi-common3, AbstractVariable: libavahi-glib1, AbstractVariable: libavahi-qt3-1, AbstractVariable: libavc1394-0, AbstractVariable: libawn0, AbstractVariable: libbatteries-ocaml-dev, AbstractVariable: libbatteries-ocaml-doc, AbstractVariable: libblas3gf, AbstractVariable: libbluetooth-dev, AbstractVariable: libbluetooth2, AbstractVariable: libbonobo2-0, AbstractVariable: libbonobo2-common, AbstractVariable: libbonoboui2-0, AbstractVariable: libbonoboui2-common, AbstractVariable: libbsd-dev, AbstractVariable: libbsd0, AbstractVariable: libc-bin, AbstractVariable: libc-client2007e, AbstractVariable: libc-dev-bin, AbstractVariable: libc6, AbstractVariable: libc6-dev, AbstractVariable: libcaca0, AbstractVariable: libcamomile-ocaml-data, AbstractVariable: libcamomile-ocaml-dev, AbstractVariable: libcompress-raw-zlib-perl, AbstractVariable: libcompress-zlib-perl, AbstractVariable: libcryptgps-ocaml-dev, AbstractVariable: libcucul0, AbstractVariable: libcups2, AbstractVariable: libcurl-ocaml, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libdb4.7, AbstractVariable: libdb4.8, AbstractVariable: libdbd-mysql-perl, AbstractVariable: libdbi-perl, AbstractVariable: libdbus-1-3, AbstractVariable: libdbus-glib-1-2, AbstractVariable: libdrm2, AbstractVariable: libecj-java, AbstractVariable: libesd0, AbstractVariable: libexif12, AbstractVariable: libexpat-ocaml, AbstractVariable: libexpat-ocaml-dev, AbstractVariable: libfam0, AbstractVariable: libffi-dev, AbstractVariable: libffi5, AbstractVariable: libfindlib-ocaml, AbstractVariable: libfindlib-ocaml-dev, AbstractVariable: libflac8, AbstractVariable: libfontconfig1, AbstractVariable: libfreebob0, AbstractVariable: libgail-common, AbstractVariable: libgail18, AbstractVariable: libgconf2-4, AbstractVariable: libgcrypt11, AbstractVariable: libgcrypt11-dev, AbstractVariable: libgfortran3, AbstractVariable: libghc6-binary-dev, AbstractVariable: libghc6-dataenc-dev, AbstractVariable: libghc6-mmap0.4-dev, AbstractVariable: libghc6-mtl-dev, AbstractVariable: libghc6-zlib-dev, AbstractVariable: libgimp2.0, AbstractVariable: libgl1-mesa-glx, AbstractVariable: libglade2-0, AbstractVariable: libglib-perl, AbstractVariable: libglib2.0-0, AbstractVariable: libglib2.0-dev, AbstractVariable: libglu1-mesa, AbstractVariable: libgmp3-dev, AbstractVariable: libgmpxx4ldbl, AbstractVariable: libgnome-desktop-2, AbstractVariable: libgnome-keyring0, AbstractVariable: libgnome2-0, AbstractVariable: libgnome2-common, AbstractVariable: libgnome2-vfs-perl, AbstractVariable: libgnomecanvas2-0, AbstractVariable: libgnomecanvas2-common, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomeui-common, AbstractVariable: libgnomevfs2-0, AbstractVariable: libgnomevfs2-common, AbstractVariable: libgnutls-dev, AbstractVariable: libgnutls13, AbstractVariable: libgnutls26, AbstractVariable: libgpg-error-dev, AbstractVariable: libgpg-error0, AbstractVariable: libgssapi-krb5-2, AbstractVariable: libgstreamer0.10-0, AbstractVariable: libgtk2.0-0, AbstractVariable: libgtkhtml2-0, AbstractVariable: libhal-storage1, AbstractVariable: libhal1, AbstractVariable: libhdf5-lam-1.8.4, AbstractVariable: libhpricot-ruby1.9, AbstractVariable: libidl0, AbstractVariable: libiec61883-0, AbstractVariable: libimlib2, AbstractVariable: libio-compress-base-perl, AbstractVariable: libio-compress-zlib-perl, AbstractVariable: libio-socket-ssl-perl, AbstractVariable: libjack0, AbstractVariable: libjhdf5-jni, AbstractVariable: libk5crypto3, AbstractVariable: libkrb5-3, AbstractVariable: libkrb5support0, AbstractVariable: liblam4, AbstractVariable: liblapack3gf, AbstractVariable: libldap2, AbstractVariable: libltdl7, AbstractVariable: liblua5.1-lpeg2, AbstractVariable: liblua5.1-socket-dev, AbstractVariable: liblua5.1-socket2, AbstractVariable: liblua50, AbstractVariable: liblualib50, AbstractVariable: liblwp-dev, AbstractVariable: liblwp2, AbstractVariable: liblzo-dev, AbstractVariable: liblzo1, AbstractVariable: libmad0, AbstractVariable: libmilter1.0.1, AbstractVariable: libmng1, AbstractVariable: libmodplug0c2, AbstractVariable: libmpcdec3, AbstractVariable: libmysqlclient15off, AbstractVariable: libmysqlclient16, AbstractVariable: libncurses5, AbstractVariable: libncurses5-dev, AbstractVariable: libnet-ldap-perl, AbstractVariable: libocamlnet-ocaml, AbstractVariable: libocamlnet-ocaml-dev, AbstractVariable: libonig2, AbstractVariable: libopenobex1, AbstractVariable: libopenobex1-dev, AbstractVariable: libopenraw1, AbstractVariable: libopenrawgnome1, AbstractVariable: libopenssl-ruby1.9, AbstractVariable: liborbit2, AbstractVariable: libpanel-applet2-0, AbstractVariable: libpaper-utils, AbstractVariable: libpcre-ocaml, AbstractVariable: libpcre-ocaml-dev, AbstractVariable: libpcre3, AbstractVariable: libpcre3-dev, AbstractVariable: libpcrecpp0, AbstractVariable: libperl5.10, AbstractVariable: libpoldiff1, AbstractVariable: libpoppler-glib3, AbstractVariable: libpoppler3, AbstractVariable: libpopt-dev, AbstractVariable: libpopt0, AbstractVariable: libpostproc51, AbstractVariable: libpq5, AbstractVariable: libpulse0, AbstractVariable: libpxp-ocaml-dev, AbstractVariable: libqdbm14, AbstractVariable: libqpol1, AbstractVariable: libqt3-mt, AbstractVariable: libqt4-network, AbstractVariable: libqtcore4, AbstractVariable: libreadline-java, AbstractVariable: libreadline6, AbstractVariable: libruby1.9, AbstractVariable: libsmbclient, AbstractVariable: libsmokeqtcore4-3, AbstractVariable: libsoup2.2-8, AbstractVariable: libsoup2.2-dev, AbstractVariable: libspeex1, AbstractVariable: libssl0.9.8, AbstractVariable: libstartup-notification0, AbstractVariable: libstdc++6-4.3-dev, AbstractVariable: libsybdb5, AbstractVariable: libsyncml-dev, AbstractVariable: libsyncml0, AbstractVariable: libtasn1-3, AbstractVariable: libtasn1-3-dev, AbstractVariable: libusb-dev, AbstractVariable: libuuid1, AbstractVariable: libvorbisfile3, AbstractVariable: libwavpack1, AbstractVariable: libwbxml2-0, AbstractVariable: libwbxml2-dev, AbstractVariable: libwnck-common, AbstractVariable: libwnck22, AbstractVariable: libwww-perl, AbstractVariable: libxaw7, AbstractVariable: libxcb-shape0, AbstractVariable: libxcb-shm0, AbstractVariable: libxcb-xv0, AbstractVariable: libxine1-bin, AbstractVariable: libxine1-console, AbstractVariable: libxine1-ffmpeg, AbstractVariable: libxine1-gnome, AbstractVariable: libxine1-misc-plugins, AbstractVariable: libxine1-x, AbstractVariable: libxml2, AbstractVariable: libxml2-dev, AbstractVariable: libxmu6, AbstractVariable: libxrandr2, AbstractVariable: libxres1, AbstractVariable: libxslt1.1, AbstractVariable: libxv1, AbstractVariable: libxvmc1, AbstractVariable: libxxf86vm1, AbstractVariable: locales, AbstractVariable: lwp-dbg, AbstractVariable: mailx, AbstractVariable: menu-xdg, AbstractVariable: mysql-client, AbstractVariable: mysql-client-5.0, AbstractVariable: mysql-client-5.1, AbstractVariable: mysql-common, AbstractVariable: nagios-plugins-standard, AbstractVariable: ncurses-bin, AbstractVariable: netbase, AbstractVariable: nfs-common, AbstractVariable: nscd, AbstractVariable: ntpdate, AbstractVariable: ocaml-base-nox, AbstractVariable: ocaml-compiler-libs, AbstractVariable: ocaml-findlib, AbstractVariable: ocaml-interp, AbstractVariable: ocaml-nox, AbstractVariable: ocaml-ulex, AbstractVariable: ocaml-ulex08, AbstractVariable: oss-compat, AbstractVariable: pennmush-common, AbstractVariable: pennmush-mysql, AbstractVariable: perl, AbstractVariable: perl-base, AbstractVariable: perl-modules, AbstractVariable: php5-cgi, AbstractVariable: php5-cli, AbstractVariable: php5-common, AbstractVariable: php5-gd, AbstractVariable: php5-imap, AbstractVariable: php5-ldap, AbstractVariable: php5-mcrypt, AbstractVariable: php5-memcache, AbstractVariable: php5-mhash, AbstractVariable: php5-mysql, AbstractVariable: php5-recode, AbstractVariable: postfix, AbstractVariable: python-awn, AbstractVariable: python-central, AbstractVariable: python-mysqldb, AbstractVariable: python-pymssql, AbstractVariable: python-subversion, AbstractVariable: python-svn, AbstractVariable: r-base-core, AbstractVariable: r-cran-snow, AbstractVariable: rlwrap, AbstractVariable: ruby1.9, AbstractVariable: shared-mime-info, AbstractVariable: spamassassin, AbstractVariable: spampd, AbstractVariable: tcl8.4, AbstractVariable: telnet, AbstractVariable: tk8.4, AbstractVariable: trac, AbstractVariable: viewcvs, AbstractVariable: viewvc, AbstractVariable: x11-xserver-utils, AbstractVariable: xcompmgr, AbstractVariable: xmail, AbstractVariable: xvt, AbstractVariable: yorick, AbstractVariable: yorick-data, AbstractVariable: yorick-yeti, AbstractVariable: zip] # starts : 142 # conflicts : 378444 # decisions : 1914315 # propagations : 603468171 # inspects : 1331330036 # learnt literals : 87 # learnt binary clauses : 375 # learnt ternary clauses : 45 # learnt clauses : 378357 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 1341824 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 23 # 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) : 2178561.860340863 # non guided choices 14983 # learnt constraints type #Solving done (282.621s). #Solution contains:858