HEAD is now at 0e68ffa initial deployement # Checking available version of Java # Java(TM) SE Runtime Environment (build 1.6.0_12-b04) # Running really p2cudf #Solver launched on Mon Jul 05 09:51:28 UTC 2010 #Using input file /home/misc2010/data/2010/easy/randea6106.cudf #Using ouput file /home/misc2010/tmp/201007050905/p2cudf-trendy-1.6/randea6106.cudf.easy.result #Objective function trendy #Timeout 280s #java.runtime.name Java(TM) SE Runtime Environment #java.vm.name Java HotSpot(TM) Server VM #java.vm.version 11.2-b01 #java.vm.vendor Sun Microsystems Inc. #sun.arch.data.model 32 #java.version 1.6.0_12 #os.name Linux #os.version 2.6.18-6-xen-amd64 #os.arch i386 #Free memory 721951896 #Max memory 725876736 #Total memory 725876736 #Number of processors 1 #Parsing ... #Time to parse:2283 #Parsing done (2.283s). #Solving ... #Request size: 1665 #Number of packages after slice: 3094 #Slice efficiency: 91% ## 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@1aa57fb # 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, trendy # p cnf 12472 37922 # Current objective function value: 1256195273431(0.961s) # Current objective function value: 1256195262481(1.561s) # Current objective function value: 1256195251520(1.811s) # Trendy criteria value: -61, -0, -21, -442 # Proof: [AbstractVariable: apt-listbugs, AbstractVariable: apt-listchanges, AbstractVariable: apt-xapian-index, AbstractVariable: clisp, AbstractVariable: dasher, AbstractVariable: deskbar-applet, AbstractVariable: f-spot, AbstractVariable: gnome-about, AbstractVariable: gnome-accessibility, AbstractVariable: gnome-applets, AbstractVariable: gnome-core, AbstractVariable: gnome-keyring-manager, AbstractVariable: gnome-mag, AbstractVariable: gnome-orca, AbstractVariable: gnome-panel, AbstractVariable: gnome-screensaver, AbstractVariable: gnome-session, AbstractVariable: graphviz, AbstractVariable: gstreamer0.10-plugins-bad, AbstractVariable: gvfs-backends, AbstractVariable: krb5-multidev, AbstractVariable: libcurl-ocaml-dev, AbstractVariable: libcurl4-gnutls-dev, AbstractVariable: libdc1394-22, AbstractVariable: libdpkg-ruby1.8, AbstractVariable: libgettext-ruby1.8, AbstractVariable: libgnome2-perl, AbstractVariable: libgnome2.24-cil, AbstractVariable: libgnomeui-0, AbstractVariable: libgnomeui-common, AbstractVariable: libgvpr1, AbstractVariable: libhttp-access2-ruby1.8, AbstractVariable: libhttpclient-ruby1.8, AbstractVariable: libimobiledevice1, AbstractVariable: libkadm5clnt-mit7, AbstractVariable: libkrb5-dev, AbstractVariable: liblocale-ruby1.8, AbstractVariable: libneon27-gnutls-dev, AbstractVariable: libopenssl-ruby1.8, AbstractVariable: libplist1, AbstractVariable: libpostgresql-ocaml-dev, AbstractVariable: libpq-dev, AbstractVariable: librpm-dev, AbstractVariable: libruby, AbstractVariable: libruby1.8, AbstractVariable: libsigsegv0, AbstractVariable: libuconv-ruby1.8, AbstractVariable: libxml-parser-ruby1.8, AbstractVariable: locales, AbstractVariable: miro, AbstractVariable: python-apt, AbstractVariable: python-gnome2, AbstractVariable: python-gnomeapplet, AbstractVariable: python-pyatspi, AbstractVariable: rhythmbox, AbstractVariable: rhythmbox-plugins, AbstractVariable: ruby, AbstractVariable: ruby1.8, AbstractVariable: vim-addon-manager, AbstractVariable: xchat-gnome, AbstractVariable: xindy, AbstractVariable: 29147324, AbstractVariable: 21173056, AbstractVariable: 2859291, AbstractVariable: 8897128, AbstractVariable: 14525019, AbstractVariable: 2228437, AbstractVariable: 18725445, AbstractVariable: 26882784, AbstractVariable: 28652556, AbstractVariable: 19098837, AbstractVariable: 274614, AbstractVariable: 25018827, AbstractVariable: 3387681, AbstractVariable: 25054702, AbstractVariable: 33108879, AbstractVariable: 173823, AbstractVariable: 13101223, AbstractVariable: 11894426, AbstractVariable: 16606885, AbstractVariable: 10168913, AbstractVariable: 12437939, AbstractVariable: 9menu, AbstractVariable: a2ps, AbstractVariable: amiwm, AbstractVariable: anthy-common, AbstractVariable: aptitude-doc-fi, AbstractVariable: aqbanking-tools, AbstractVariable: aspell, AbstractVariable: aspell-bg, AbstractVariable: aterm, AbstractVariable: aterm-ml, AbstractVariable: audacious, AbstractVariable: audacious-plugins, AbstractVariable: aumix-common, AbstractVariable: aumix-gtk, AbstractVariable: autopoint, AbstractVariable: awesome, AbstractVariable: bcc, AbstractVariable: bcron, AbstractVariable: bin86, AbstractVariable: bluez-alsa, AbstractVariable: bluez-cups, AbstractVariable: bluez-gstreamer, AbstractVariable: bzr, AbstractVariable: bzr-upload, AbstractVariable: bzrtools, AbstractVariable: ca-certificates-java, AbstractVariable: cabextract, AbstractVariable: cdparanoia, AbstractVariable: citadel-server, AbstractVariable: cl-swank, AbstractVariable: conkeror, AbstractVariable: conkeror-spawn-process-helper, AbstractVariable: cpp-4.1, AbstractVariable: db4.6-util, AbstractVariable: debootstrap, AbstractVariable: distcc, AbstractVariable: dkms, AbstractVariable: dmraid, AbstractVariable: dolphin, AbstractVariable: dracut, AbstractVariable: dwm, AbstractVariable: dwm-tools, AbstractVariable: e16, AbstractVariable: e16-data, AbstractVariable: elks-libc, AbstractVariable: emacs22, AbstractVariable: emacs22-bin-common, AbstractVariable: emacs22-common, AbstractVariable: emacsen-common, AbstractVariable: exfalso, AbstractVariable: exo-utils, AbstractVariable: fancontrol, AbstractVariable: festival, AbstractVariable: festival-hi, AbstractVariable: festival-mr, AbstractVariable: festival-te, AbstractVariable: festlex-ifd, AbstractVariable: festvox-hi-nsk, AbstractVariable: festvox-italp16k, AbstractVariable: festvox-itapc16k, AbstractVariable: festvox-mr-nsk, AbstractVariable: festvox-suopuhe-common, AbstractVariable: festvox-suopuhe-lj, AbstractVariable: festvox-suopuhe-mv, AbstractVariable: festvox-te-nsk, AbstractVariable: fetchmail, AbstractVariable: fgetty, AbstractVariable: fglrx-atieventsd, AbstractVariable: fglrx-driver, AbstractVariable: fglrx-glx, AbstractVariable: fglrx-glx-ia32, AbstractVariable: fglrx-source, AbstractVariable: fluxbox, AbstractVariable: flwm, AbstractVariable: fortune-mod, AbstractVariable: fortunes, AbstractVariable: fortunes-debian-hints, AbstractVariable: fortunes-min, AbstractVariable: fortunes-off, AbstractVariable: fvwm, AbstractVariable: fvwm-crystal, AbstractVariable: fvwm-icons, AbstractVariable: gcc-4.1, AbstractVariable: gcc-4.1-base, AbstractVariable: ghostscript-x, AbstractVariable: gir1.0-mutter-2.29, AbstractVariable: gnome-audio, AbstractVariable: gnome-shell, AbstractVariable: gnome3-session, AbstractVariable: gnustep-base-common, AbstractVariable: gnustep-base-runtime, AbstractVariable: gnustep-common, AbstractVariable: gsfonts-x11, AbstractVariable: gstreamer0.10-gnomevfs, AbstractVariable: gstreamer0.10-pulseaudio, AbstractVariable: gtk2-engines-pixbuf, AbstractVariable: gv, AbstractVariable: habak, AbstractVariable: hunspell-uz, AbstractVariable: i3-wm, AbstractVariable: ia32-sun-java6-bin, AbstractVariable: ice33-slice, AbstractVariable: ice33-translators, AbstractVariable: icedtea-6-jre-cacao, AbstractVariable: icewm-common, AbstractVariable: ipsvd, AbstractVariable: java-common, AbstractVariable: jed, AbstractVariable: jed-common, AbstractVariable: jed-extra, AbstractVariable: k3b, AbstractVariable: k3b-data, AbstractVariable: kaboom, AbstractVariable: kbuild, AbstractVariable: kdebase-bin, AbstractVariable: kdebase-data, AbstractVariable: kdebase-runtime, AbstractVariable: kdebase-runtime-data, AbstractVariable: kdelibs-bin, AbstractVariable: kdelibs5-data, AbstractVariable: kdelibs5-plugins, AbstractVariable: kdoctools, AbstractVariable: kernel-package, AbstractVariable: kfind, AbstractVariable: konqueror, AbstractVariable: konqueror-nsplugins, AbstractVariable: kwwidgets-examples, AbstractVariable: libaccess-bridge-java, AbstractVariable: libaccess-bridge-java-jni, AbstractVariable: libafterimage0, AbstractVariable: libalgorithm-diff-perl, AbstractVariable: libalgorithm-merge-perl, AbstractVariable: libanthy0, AbstractVariable: libanyevent-i3-perl, AbstractVariable: libanyevent-perl, AbstractVariable: libaqbanking-data, AbstractVariable: libaqbanking-plugins-libgwenhywfar47, AbstractVariable: libaqbanking29, AbstractVariable: libaqbanking29-plugins, AbstractVariable: libaqbanking29-plugins-qt, AbstractVariable: libaqhbci17, AbstractVariable: libaqofxconnect5, AbstractVariable: libasound2-plugins, AbstractVariable: libasync-interrupt-perl, AbstractVariable: libatm1, AbstractVariable: libattica0, AbstractVariable: libaudclient2, AbstractVariable: libaudcore1, AbstractVariable: libaudid3tag2, AbstractVariable: libavahi-compat-libdnssd1, AbstractVariable: libbg1, AbstractVariable: libbg1-doc, AbstractVariable: libbinio1ldbl, AbstractVariable: libcitadel2, AbstractVariable: libclucene0ldbl, AbstractVariable: libcommon-sense-perl, AbstractVariable: libcue1, AbstractVariable: libdigest-hmac-perl, AbstractVariable: libdmraid1.0.0.rc16, AbstractVariable: libestools1.2, AbstractVariable: libev3, AbstractVariable: libexo-0.3-0, AbstractVariable: libexo-common, AbstractVariable: libflac++6, AbstractVariable: libfltk1.1, AbstractVariable: libfluidsynth1, AbstractVariable: libfont-afm-perl, AbstractVariable: libgjs0a, AbstractVariable: libgl1-mesa-dev, AbstractVariable: libglu1-mesa-dev, AbstractVariable: libgnustep-base1.19, AbstractVariable: libgpod-common, AbstractVariable: libgraphicsmagick3, AbstractVariable: libgsasl7, AbstractVariable: libgwenhywfar47, AbstractVariable: libhtml-format-perl, AbstractVariable: libhubbub0, AbstractVariable: libiceutil33, AbstractVariable: libio-socket-inet6-perl, AbstractVariable: libiodbc2, AbstractVariable: libjs-mootools, AbstractVariable: libjson-perl, AbstractVariable: libjson-xs-perl, AbstractVariable: libk3b6, AbstractVariable: libk3b6-extracodecs, AbstractVariable: libkcddb4, AbstractVariable: libkde3support4, AbstractVariable: libkdecore5, AbstractVariable: libkdesu5, AbstractVariable: libkdeui5, AbstractVariable: libkdnssd4, AbstractVariable: libkeybinder0, AbstractVariable: libkfile4, AbstractVariable: libkhtml5, AbstractVariable: libkio5, AbstractVariable: libkjsapi4, AbstractVariable: libkjsembed4, AbstractVariable: libkmediaplayer4, AbstractVariable: libknewstuff2-4, AbstractVariable: libknewstuff3-4, AbstractVariable: libknotifyconfig4, AbstractVariable: libkntlm4, AbstractVariable: libkonq5, AbstractVariable: libkonq5-templates, AbstractVariable: libkonqsidebarplugin4a, AbstractVariable: libkparts4, AbstractVariable: libkpty4, AbstractVariable: libkrosscore4, AbstractVariable: libktexteditor4, AbstractVariable: libktoblzcheck1c2a, AbstractVariable: libkutils4, AbstractVariable: liblash2, AbstractVariable: libllvm2.7, AbstractVariable: libltdl-dev, AbstractVariable: libm17n-0, AbstractVariable: libmail-spf-perl, AbstractVariable: libmatrixssl1.8, AbstractVariable: libmcpp0, AbstractVariable: libmcs1, AbstractVariable: libmowgli1, AbstractVariable: libmpdclient2, AbstractVariable: libmutter-private0, AbstractVariable: libnepomuk4, AbstractVariable: libnepomukquery4a, AbstractVariable: libnet-dns-perl, AbstractVariable: libnet-ip-perl, AbstractVariable: libnetaddr-ip-perl, AbstractVariable: libnsbmp0, AbstractVariable: libnsgif0, AbstractVariable: libntlm0, AbstractVariable: libobjc2, AbstractVariable: libobparser21, AbstractVariable: libobrender21, AbstractVariable: libonig2, AbstractVariable: libotf0, AbstractVariable: libpaper-utils, AbstractVariable: libparserutils0, AbstractVariable: libphonon4, AbstractVariable: libplasma3, AbstractVariable: libpolkit-qt-1-0, AbstractVariable: libpulse-browse0, AbstractVariable: libqbanking8, AbstractVariable: libqca2, AbstractVariable: libqt3-mt, AbstractVariable: libqt4-dev, AbstractVariable: libqt4-help, AbstractVariable: libqt4-multimedia, AbstractVariable: libqt4-opengl-dev, AbstractVariable: libqt4-scripttools, AbstractVariable: libqt4-webkit, AbstractVariable: libqt4-xmlpatterns, AbstractVariable: libqtscript4-core, AbstractVariable: libqtscript4-network, AbstractVariable: libqwtplot3d-qt4-0, AbstractVariable: libqwtplot3d-qt4-dev, AbstractVariable: librecode0, AbstractVariable: libresid-builder0c2a, AbstractVariable: librplay3, AbstractVariable: libsidplay2, AbstractVariable: libsieve2-1, AbstractVariable: libslang2-modules, AbstractVariable: libslice33, AbstractVariable: libsocket6-perl, AbstractVariable: libsolid4, AbstractVariable: libsoprano4, AbstractVariable: libssh-4, AbstractVariable: libstreamanalyzer0, AbstractVariable: libstreams0, AbstractVariable: libstroke0, AbstractVariable: libthreadweaver4, AbstractVariable: libthunar-vfs-1-2, AbstractVariable: libtool, AbstractVariable: libvirtodbc0, AbstractVariable: libvisual-0.4-plugins, AbstractVariable: libvncserver0, AbstractVariable: libwmf-bin, AbstractVariable: libx11-protocol-perl, AbstractVariable: libxcb-icccm1, AbstractVariable: libxcb-image0, AbstractVariable: libxcb-property1, AbstractVariable: libxcb-randr0, AbstractVariable: libxcb-shape0, AbstractVariable: libxcb-shm0, AbstractVariable: libxcb-xinerama0, AbstractVariable: libxcb-xtest0, AbstractVariable: libxcb-xv0, AbstractVariable: libxdg-basedir1, AbstractVariable: libxfce4menu-0.1-0, AbstractVariable: libxfce4util-bin, AbstractVariable: libxfce4util-common, AbstractVariable: libxfce4util4, AbstractVariable: libxfcegui4-4, AbstractVariable: libxfconf-0-2, AbstractVariable: libxine1, AbstractVariable: libxine1-bin, AbstractVariable: libxine1-console, AbstractVariable: libxine1-ffmpeg, AbstractVariable: libxine1-misc-plugins, AbstractVariable: libxine1-x, AbstractVariable: libyajl1, AbstractVariable: libzeroc-ice33, AbstractVariable: linux-image-2.6.32-5-openvz-amd64, AbstractVariable: linux-image-2.6.32-5-vserver-amd64, AbstractVariable: linux-image-2.6.32-5-xen-amd64, AbstractVariable: llvm-2.7, AbstractVariable: llvm-2.7-dev, AbstractVariable: llvm-2.7-examples, AbstractVariable: llvm-2.7-runtime, AbstractVariable: locales-all, AbstractVariable: lxsession, AbstractVariable: m17n-contrib, AbstractVariable: m17n-db, AbstractVariable: mdadm, AbstractVariable: mercurial, AbstractVariable: mercurial-common, AbstractVariable: mesa-common-dev, AbstractVariable: mesa-utils, AbstractVariable: midori, AbstractVariable: mlterm, AbstractVariable: mlterm-common, AbstractVariable: mlterm-tools, AbstractVariable: mpc, AbstractVariable: msmtp, AbstractVariable: mutter, AbstractVariable: mutter-common, AbstractVariable: navit-graphics-qt-qpainter, AbstractVariable: navit-gui-gtk, AbstractVariable: netsurf-framebuffer-common, AbstractVariable: netsurf-gtk, AbstractVariable: netsurf-linuxfb, AbstractVariable: netsurf-sdl, AbstractVariable: netsurf-vnc, AbstractVariable: odbcinst, AbstractVariable: odbcinst1debian2, AbstractVariable: openbox, AbstractVariable: openbox-themes, AbstractVariable: openjdk-6-jre-headless, AbstractVariable: openjdk-6-jre-lib, AbstractVariable: openoffice.org-emailmerge, AbstractVariable: openoffice.org-filter-binfilter, AbstractVariable: openssh-server, AbstractVariable: oss-compat, AbstractVariable: oxygen-icon-theme, AbstractVariable: perl-tk, AbstractVariable: perlmagick, AbstractVariable: phonon, AbstractVariable: phonon-backend-gstreamer, AbstractVariable: plasma-scriptengine-javascript, AbstractVariable: psutils, AbstractVariable: pulseaudio, AbstractVariable: pulseaudio-esound-compat, AbstractVariable: pulseaudio-module-x11, AbstractVariable: pulseaudio-utils, AbstractVariable: python-cddb, AbstractVariable: python-configobj, AbstractVariable: python-crypto, AbstractVariable: python-django-mumble, AbstractVariable: python-gpod, AbstractVariable: python-keybinder, AbstractVariable: python-musicbrainz2, AbstractVariable: python-mutagen, AbstractVariable: python-paramiko, AbstractVariable: python-uno, AbstractVariable: python-zeroc-ice, AbstractVariable: qt4-qmake, AbstractVariable: quodlibet, AbstractVariable: quodlibet-ext, AbstractVariable: quodlibet-plugins, AbstractVariable: ratpoison, AbstractVariable: re2c, AbstractVariable: rox-filer, AbstractVariable: roxterm, AbstractVariable: runit, AbstractVariable: rxvt, AbstractVariable: rxvt-ml, AbstractVariable: sbcl, AbstractVariable: scrotwm, AbstractVariable: shared-desktop-ontologies, AbstractVariable: slime, AbstractVariable: slsh, AbstractVariable: socklog, AbstractVariable: soprano-daemon, AbstractVariable: spamassassin, AbstractVariable: spamc, AbstractVariable: stalonetray, AbstractVariable: sun-java6-bin, AbstractVariable: sun-java6-jre, AbstractVariable: tango-icon-theme, AbstractVariable: terminator, AbstractVariable: texlive-fonts-recommended-doc, AbstractVariable: texlive-humanities-doc, AbstractVariable: texlive-latex-extra-doc, AbstractVariable: texlive-latex-recommended-doc, AbstractVariable: texlive-pictures-doc, AbstractVariable: texlive-pstricks-doc, AbstractVariable: thunar, AbstractVariable: thunar-data, AbstractVariable: thunar-volman, AbstractVariable: tightvncserver, AbstractVariable: tipa, AbstractVariable: tla, AbstractVariable: tla-doc, AbstractVariable: ttf-bitstream-vera, AbstractVariable: ttf-mscorefonts-installer, AbstractVariable: tzdata-java, AbstractVariable: ucspi-unix, AbstractVariable: ude, AbstractVariable: unixodbc, AbstractVariable: util-vserver, AbstractVariable: uwm, AbstractVariable: vcdimager, AbstractVariable: virtualbox-ose-guest-source, AbstractVariable: virtualbox-ose-guest-utils, AbstractVariable: virtualbox-ose-guest-x11, AbstractVariable: virtuoso-minimal, AbstractVariable: virtuoso-opensource-6.1-bin, AbstractVariable: virtuoso-opensource-6.1-common, AbstractVariable: vnc4server, AbstractVariable: vzctl, AbstractVariable: vzquota, AbstractVariable: wmii, AbstractVariable: wmii-doc, AbstractVariable: wodim, AbstractVariable: xaw3dg, AbstractVariable: xdg-user-dirs, AbstractVariable: xfce-keyboard-shortcuts, AbstractVariable: xfce4-panel, AbstractVariable: xfce4-session, AbstractVariable: xfce4-settings, AbstractVariable: xfce4-terminal, AbstractVariable: xfce4-utils, AbstractVariable: xfconf, AbstractVariable: xfdesktop4, AbstractVariable: xfdesktop4-data, AbstractVariable: xfonts-terminus, AbstractVariable: xfwm4, AbstractVariable: xfwm4-themes, AbstractVariable: xinput, AbstractVariable: xlockmore, AbstractVariable: xnest, AbstractVariable: xpdf-common, AbstractVariable: zeroinstall-injector] # starts : 16 # conflicts : 2380 # decisions : 195028 # propagations : 2737658 # inspects : 5037863 # learnt literals : 52 # learnt binary clauses : 176 # learnt ternary clauses : 131 # learnt clauses : 2327 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 673446 # 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) : 162887.96334860477 # non guided choices 35831 # learnt constraints type #Solving done (20.923s). #Solution contains:2002