# Solver launched on Mon Sep 03 03:06:51 UTC 2012
# Using input file /home/competition/data/upgrade/easy/rand695.cudf
# Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/dist-upgrade/upgrade/easy/rand695.cudf.result
# Objective function -notuptodate(solution),-aligned(solution,source,sourceversion),-unsat_recommends(solution),-count(new)
# Timeout 285s
# java.runtime.name	OpenJDK Runtime Environment
# java.vm.name		OpenJDK 64-Bit Server VM
# java.vm.version	20.0-b12
# java.vm.vendor	Sun Microsystems Inc.
# sun.arch.data.model	64
# java.version		1.6.0_24
# os.name		Linux
# os.version		2.6.32-5-amd64
# os.arch		amd64
# Free memory 		655262992
# Max memory 		658898944
# Total memory 		658898944
# Number of processors 	1
# Parsing ...
# Time to parse:5404
# Parsing done (5.411s).
# Solving ...
# Request size: 1012
# Number of  packages after slice: 8063
# Slice efficiency: 85%
# --- Begin Solver configuration ---
# org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@5220be79
# 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
# Simple reason simplification
# luby style (SATZ_rand, TiniSAT) restarts strategy with factor 512
# Glucose 2 learned constraints deletion strategy
# timeout=285s
# DB Simplification allowed=false
# --- End Solver configuration ---
# Optimization function: User defined:-notuptodate(solution),-aligned(solution,source,sourceversion),-unsat_recommends(solution),-count(new)
Skipping unknown criteria:-notuptodate()
# criteria notuptodate() size is 0 using new vars 11249 to 11249
# criteria aligned(source,sourceversion) size is 5792
Skipping unknown criteria:-unsat_recommends()
# criteria unsat_recommends() size is 5792 using new vars 11249 to 14155
# criteria new size is 2919 using new vars 14155 to 17074
# p cnf 17073 87074
# Found optimal criterion number 1
# Current objective function value: 11(1.264s)
# Current objective function value: 9(1.615s)
# Current objective function value: 5(1.906s)
# cleaning 2558 clauses out of 5128 with flag 10524/5167
# cleaning 4281 clauses out of 8570 with flag 23004/11167
# cleaning 5638 clauses out of 11288 with flag 37589/18166
# cleaning 6819 clauses out of 13651 with flag 54174/26167
# cleaning 7916 clauses out of 15831 with flag 72949/35166
# cleaning 8958 clauses out of 17915 with flag 93695/45166
# cleaning 9979 clauses out of 19958 with flag 117573/56167
# cleaning 10983 clauses out of 21978 with flag 142895/68166
# cleaning 11987 clauses out of 23995 with flag 170062/81166
# cleaning 13001 clauses out of 26008 with flag 199669/95166
# cleaning 13996 clauses out of 28007 with flag 231283/110166
# cleaning 14996 clauses out of 30012 with flag 265439/126167
# cleaning 15999 clauses out of 32016 with flag 301029/143167
# cleaning 17003 clauses out of 34016 with flag 338816/161166
# cleaning 17994 clauses out of 36014 with flag 379271/180167
# cleaning 19004 clauses out of 38019 with flag 421333/200166
# cleaning 20002 clauses out of 40015 with flag 465421/221166
# cleaning 21007 clauses out of 42013 with flag 511440/243166
# cleaning 21993 clauses out of 44007 with flag 559935/266167
# cleaning 22999 clauses out of 46014 with flag 610418/290167
# cleaning 24004 clauses out of 48014 with flag 662753/315166
# cleaning 25005 clauses out of 50011 with flag 716844/341167
# cleaning 25996 clauses out of 52005 with flag 773128/368166
# cleaning 27000 clauses out of 54009 with flag 838749/396166
# cleaning 27992 clauses out of 56010 with flag 906166/425167
# cleaning 29001 clauses out of 58018 with flag 972172/455167
# Solver timed out after 285.521s)
# -new criteria value: 574
# Newly installed packages: [9menu, a2ps, aewm, af, altgcc, app-install-data, aspell, aspell-bin, aspell-en, aspell-es, aspell-ukr, blam, busybox, ca-certificates, cdcd, cdebconf, cdrdao, chimera2, clamav-data, classpath-tools, cli-common, console-terminus, cpp-4.1, cracklib-runtime, cramfsprogs, dash, dbus, dbus-x11, debconf-english, debian-archive-keyring, devfsd, discover1-data, dmz-cursor-theme, dvi2tty, dviutils, egroupware-egw-pear, epdfview, epos-ktd, epos-lpc, epos-ptd, fastjar, festival, festlex-cmu, festlex-poslex, festvox-kallpc16k, festvox-kdlpc8k, flwm, fontconfig-config, fruit, gamin, gawk, gcc-4.1-base, gcc-4.3-base, gconf2-common, gdk-imlib11, gij-3.3, gnome-audio, gnome-bin, gnome-games-extra-data, gnome-libs-data, gnome-netstatus-applet, gnome-spell, gnustep-back, gnustep-base-common, gnustep-common, gnustep-gui-common, gnustep-ppd, gpgv, grep-dctrl, gs-esp, gtk2-engines, guile-1.6, guile-library, hal-info, hardinfo, heirloom-mailx, host, hunspell-ar, hunspell-en-us, hunspell-se, hunspell-uz, industrial-cursor-theme, iportuguese, ispell, jade, jwm, kdelibs4c2a, krb4-config, kterm, lapack3, larswm, latex-xcolor, ldso, libacr38u, libalut0, libao2, libapr1, libaprutil1, libarchive1, libart2, libart2.0-cil, libarts1c2a, libasyncns0, libatk1.0-data, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-glib1, libavahi-qt3-1, libavahi-ui0, libavc1394-0, libbcel-java, libbeecrypt6, libbinio1ldbl, libblas3gf, libboost-python1.34.1, libcairo-perl, libcairo2, libcairomm-1.0-1, libcamel1.2-11, libcanna1g, libcap2, libccid, libcdaudio1, libcddb2, libcgi-ssi-parser-perl, libcitadel1, libclass-accessor-perl, libclucene0ldbl, libcolorblind0, libcompress-raw-zlib-perl, libcompress-zlib-perl, libcrack2, libcteco50000, libcups2, libcupsimage2, libcupsys2, libcxxtools6, libdatrie0, libdb2, libdb4.4, libdb4.5, libdb4.6, libdbd-mysql-perl, libdbi-perl, libdbus-1-3, libdbus-glib-1-2, libdbus-qt-1-1c2, libdc1394-13, libdebian-installer4, libdevel-symdump-perl, libdigest-hmac-perl, libdigest-sha1-perl, libdirectfb-1.0-0, libdirectfb-extra, libdmx1, libdrm2, libeb12, libecal1.2-6, libedataserver1.2-7, libedataserver1.2-9, libedit2, libelfg0, libenchant1c2a, libept0, liberror-perl, libesd-alsa0, libestools1.2, libevtlog0, libexempi3, libfaad0, libffcall1, libffi5, libfile-ncopy-perl, libfile-remove-perl, libfltk1.1, libfont-afm-perl, libfontenc1, libforms1, libfreebob0, libfreezethaw-perl, libfs6, libfsplib0, libg2c0, libgalago3, libgamin0, libgcj-common, libgcj4, libgconf2.0-cil, libgcr410, libgd-gd2-noxpm-perl, libgd-text-perl, libgd2-xpm, libgdk-pixbuf2, libgdome2-0, libgdome2-cpp-smart0c2a, libgecko2.0-cil, libgfortran3, libggz2, libgif4, libgl1-mesa-glide3, libglade2.0-cil, libglew1, libglib-perl, libglib2.0-cil, libglib2.0-data, libglide3, libglu1-mesa, libgmime2.1, libgmp3, libgnome-vfs2.0-cil, libgnome2-vfs-perl, libgnome2.0-cil, libgnome32, libgnomeprint-bin, libgnomeprint-data, libgnomeprint15, libgnomesupport0, libgnomeui32, libgnorba27, libgnorbagtk0, libgnustep-base1.10, libgnustep-gui0.9, libgnutls13, libgnutls26, libgomp1, libgpgme6, libgsasl7, libgsmme1c2a, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtk-vnc-1.0-0, libgtk2-perl, libgtk2.0-cil, libgtkdatesview0, libgtksourceview2.0-0, libgtksourceview2.0-common, libguppi16, libgwenhywfar47, libgwrapguile1, libhal-storage1, libhal1, libhesiod0, libhtml-format-perl, libhtml-template-perl, libhunspell-1.2-0, libhyphen0, libical0, libicu36, libid3-3.8.3, libident, libiec61883-0, libilmbase6, libinotify-ruby, libinotify-ruby1.8, libio-compress-base-perl, libio-compress-zlib-perl, libio-socket-inet6-perl, libio-string-perl, libio-zlib-perl, libiptcdata0, libjack0, libjasper1, libjaxp1.2-java, libjaxp1.3-java, libkcal2b, libkdepim1a, libkeyutils1, libkleopatra1, libktnef1, libktoblzcheck1c2a, liblapack3gf, liblazy1, libldap-2.4-2, liblog4j1.2-java, libloudmouth1-0, liblua5.1-0, liblua50, liblualib50, liblzo2-2, libmail-sendmail-perl, libmail-spf-perl, libmail-spf-query-perl, libmalaga7, libmcrypt4, libmcs1, libmdbtools, libmhash2, libmikmod2, libmodplug0c2, libmoe1.5, libmono-cairo1.0-cil, libmono-corlib1.0-cil, libmono-data-tds1.0-cil, libmono-security1.0-cil, libmono-sharpzip0.84-cil, libmono-system-data1.0-cil, libmono-system-web1.0-cil, libmono-system1.0-cil, libmono0, libmono1.0-cil, libmowgli1, libmozjs0d, libmpcdec3, libmtp7, libmusicbrainz4c2a, libmx4j-java, libmyspell3c2, libmysqlclient10, libmysqlclient12, libmysqlclient15off, libnautilus-extension1, libncursesw5, libneon25, libneon26, libnet-cidr-lite-perl, libnet-daemon-perl, libnet-dbus-perl, libnet-dns-perl, libnet-ip-perl, libnet-ph-perl, libnet-snpp-perl, libnet-ssleay-perl, libnet-telnet-perl, libnetaddr-ip-perl, libnettle2, libnewt0.52, libnl1, libnotify1, libnspr4-0d, libnss3-0d, libnss3-1d, libntlm0, libobjc1, libobject-realize-later-perl, libobparser21, liboil0.3, libonig2, libopenal0, libopenal1, libopenexr6, libopensync0, liborbit0, libpaper-utils, libparse-recdescent-perl, libpcap0.8, libpci3, libpixman-1-0, libpkcs11-helper1, libplot2c2, libplrpc-perl, libpoppler-glib3, libpoppler3, libpopplerkit0, libportaudio0, libpq4, libpt-plugins-alsa, libpth20, libqt3-mt, libraw1394-8, libregexp-java, libruby1.6, libruby1.8, libsablot0c102, libsasl2-2, libsasl2-modules, libserf-0-0, libservlet2.3-java, libservlet2.4-java, libsexy2, libsieve2-1, libsilc-1.1-2, libslang2, libsmpeg0, libsocket6-perl, libsoup2.4-1, libsp1c2, libsplashy1, libsqlite3-0, libssh2-1, libssl0.9.8, libstdc++6, libstroke0, libsuitesparse-3.1.0, libswfdec-0.6-90, libsys-hostname-long-perl, libsysfs2, libtalloc1, libtasn1-3, libtelepathy-glib0, libtelepathy2, libthai-data, libthai0, libtie-ixhash-perl, libtotem-plparser10, libtrackerclient0, libts-0.0-0, libttf2, libufsparse, libuser-identity-perl, libuuid-perl, libvoikko1, libvte9, libwpd8c2a, libwpg-0.1-1, libwps-0.1-1, libx11-data, libxapian15, libxau6, libxcb-render-util0, libxcb-render0, libxcb-xlib0, libxcb1, libxcomposite1, libxdamage1, libxdmcp6, libxfce4mcs-client3, libxfce4mcs-manager3, libxfce4util4, libxfcegui4-4, libxfixes3, libxfont1, libxinerama1, libxkbfile1, libxklavier12, libxml-handler-trees-perl, libxml-parser-perl, libxml-perl, libxml-regexp-perl, libxml-twig-perl, libxml-xpath-perl, libxml1, libxprintapputil1, libxprintutil1, libxss1, libxt-java, libxul-common, libxul0d, libxxf86dga1, libxxf86misc1, libxxf86vm1, libzvt2.0-0, libzzip-0-12, lp-solve, lprng, lsb-base, lsb-release, lwm, lxsession-lite, lxterminal, lynx-cur, lzma, make, module-init-tools, mono-common, mono-gac, mono-jit, mono-runtime, mozilla-thunderbird, myspell-fa, myspell-hr, myspell-hy, myspell-ku, myspell-pt-br, myspell-sk, mysql-client, mysql-common, mysql-server, ncurses-term, netcat-openbsd, nginx, notification-daemon-xfce, openssl, openssl-blacklist, openvpn-blacklist, oroborus, oss-compat, pcscd, php-pear, php5-cli, php5-common, pike7.6-core, pike7.6-image, pike7.6-mysql, pm-utils, postgresql-client-7.4, postgresql-client-common, preview-latex-style, pterm, pwm, python-apt, python-cairo, python-central, python-crack, python-cracklib, python-cups, python-fpconst, python-gdata, python-gobject, python-gst0.10, python-libxml2, python-minimal, python-support, python2.5, python2.5-minimal, qvwm, ratpoison, rdesktop, readline-common, refblas3, rlpr, rox-filer, roxen4, roxterm, rsyslog, ruby1.8, sapphire, seahorse, sodipodi, ssl-cert, ssmtp, stalonetray, swfdec-gnome, swfdec-mozilla, tcl8.0, tcl8.5, telepathy-gabble, terminal, thy, timezoneconf, tinywm, tk8.5, trayer, tsclient, ttf-dejavu-core, ttf-freefont, ttf-liberation, twm, tzdata, ucspi-unix, unace, unzoo, vinagre, virtualbox-ose-guest-utils, w3c-dtd-xhtml, w9wm, wdg-html-reference, wgerman-medical, windowlab, witalian, wm2, wmii, wspanish, x11-apps, x11-common, x11-session-utils, x11-xfs-utils, x11-xkb-utils, x11-xserver-utils, x11proto-core-dev, x11proto-print-dev, xauth, xbitmaps, xcursor-themes, xfce4-mcs-manager, xfonts-encodings, xfonts-utils, xfwm4, xinit, xkb-data-legacy, xprint-utils, xterm, xutils-dev, yaird]
# starts		: 257
# conflicts		: 455167
# decisions		: 1044184
# propagations		: 68442632
# inspects		: 292584742
# shortcuts		: 0
# learnt literals	: 39
# learnt binary clauses	: 79
# learnt ternary clauses	: 37
# learnt constraints	: 455128
# ignored constraints	: 0
# root simplifications	: 0
# removed literals (reason simplification)	: 4820617
# reason swapping (by a shorter reason)	: 0
# Calls to reduceDB	: 26
# Number of update (reduction) of LBD	: 7403
# 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)	: 239805.44411703906
# non guided choices	137804
# learnt constraints type 
# org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 79
# org.sat4j.minisat.constraints.cnf.LearntWLClause => 28938
# Solving done (292.258s).
# WARNING: The solution found MIGHT NOT BE optimal
# Solution contains:850