# Solver launched on Mon Sep 03 02:58:48 UTC 2012
# Using input file /home/competition/data/upgrade/easy/rand583.cudf
# Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/dist-upgrade/upgrade/easy/rand583.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:5320
# Parsing done (5.339s).
# Solving ...
# Request size: 1012
# Number of  packages after slice: 8044
# 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 11224 to 11224
# criteria aligned(source,sourceversion) size is 5771
Skipping unknown criteria:-unsat_recommends()
# criteria unsat_recommends() size is 5771 using new vars 11224 to 14122
# criteria new size is 2905 using new vars 14122 to 17027
# p cnf 17026 86826
# Found optimal criterion number 1
# Current objective function value: 4(1.14s)
# Current objective function value: 5(1.375s)
# Current objective function value: 3(1.602s)
# cleaning 2551 clauses out of 5101 with flag 11023/5111
# cleaning 4269 clauses out of 8550 with flag 24430/11111
# cleaning 5635 clauses out of 11281 with flag 41007/18111
# cleaning 6814 clauses out of 13646 with flag 60136/26111
# cleaning 7904 clauses out of 15831 with flag 82534/35110
# cleaning 8963 clauses out of 17927 with flag 104866/45110
# cleaning 9981 clauses out of 19964 with flag 128469/56110
# cleaning 10988 clauses out of 21984 with flag 153982/68111
# cleaning 11993 clauses out of 23997 with flag 180650/81112
# cleaning 13002 clauses out of 26003 with flag 209522/95111
# cleaning 13996 clauses out of 28001 with flag 240787/110111
# cleaning 14995 clauses out of 30005 with flag 275296/126111
# cleaning 15997 clauses out of 32009 with flag 311910/143110
# cleaning 16999 clauses out of 34013 with flag 354681/161111
# cleaning 18001 clauses out of 36013 with flag 398890/180110
# cleaning 18999 clauses out of 38012 with flag 445567/200110
# cleaning 20004 clauses out of 40013 with flag 490450/221110
# cleaning 20995 clauses out of 42010 with flag 537018/243111
# cleaning 22001 clauses out of 44015 with flag 583911/266111
# cleaning 22996 clauses out of 46013 with flag 634399/290110
# cleaning 24003 clauses out of 48017 with flag 691395/315110
# cleaning 25000 clauses out of 50014 with flag 748244/341110
# cleaning 26004 clauses out of 52014 with flag 805087/368110
# cleaning 26994 clauses out of 54010 with flag 869710/396110
# cleaning 27997 clauses out of 56017 with flag 937664/425111
# cleaning 29007 clauses out of 58019 with flag 1008282/455110
# cleaning 30001 clauses out of 60012 with flag 1081196/486110
# cleaning 30999 clauses out of 62011 with flag 1152991/518110
# cleaning 32007 clauses out of 64013 with flag 1229922/551111
# cleaning 32996 clauses out of 66005 with flag 1300544/585110
# cleaning 33992 clauses out of 68010 with flag 1377174/620111
# Solver timed out after 285.091s)
# -new criteria value: 500
# Newly installed packages: [9base, 9menu, aewm, af, akregator, alsa-base, alsa-utils, altgcc, app-install-data, aspell-en, aspell-es, aspell-ukr, busybox, ca-certificates, cdcd, cdrdao, chimera2, clamav-data, classpath-tools, cli-common, console-terminus, cpp-4.1, cramfsprogs, cronosii, dash, dbus, debconf-english, debian-archive-keyring, devfsd, discover1-data, dmz-cursor-theme, dvi2tty, dviutils, elinks-lite, epdfview, epos-ktd, epos-lpc, epos-ptd, esound-clients, fastjar, festival, festlex-cmu, festlex-poslex, festvox-kallpc16k, festvox-kdlpc16k, festvox-suopuhe-common, festvox-suopuhe-mv, fontconfig-config, gawk, gcc-4.1-base, gcc-4.3-base, gconf2-common, gdk-imlib1, gdk-imlib11, ghostscript, ghostscript-x, gij-3.3, gnome-audio, gnome-backgrounds, gnome-bin, gnome-doc-utils, gnome-games-extra-data, gnome-libs-data, gnustep-back, gnustep-base-common, gnustep-common, gnustep-gui-common, gnustep-ppd, gpgv, grep-dctrl, guile-1.6, hal-info, hardinfo, hoichess, host, hunspell-ar, hunspell-en-us, hunspell-se, hunspell-uz, industrial-cursor-theme, jwm, kbd, krb4-config, ktalkd, kterm, ladcca2, lapack3, larswm, latex-xcolor, ldso, libacr38u, libalut0, libao2, libapr1, libaprutil1, libarchive1, libart2, libasyncns0, libatk1.0-data, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-glib1, libbcel-java, libbeecrypt6, libbinio1ldbl, libblas3gf, libcairo-perl, libcairo2, libcairomm-1.0-1, libcamel1.2-11, libcanna1g, libcap2, libccid, libcdaudio1, libcddb2, libcitadel1, libclass-accessor-perl, libclucene0ldbl, libcolorblind0, libcompress-zlib-perl, libcteco50000, libcups2, libcupsimage2, libcupsys2, libcxxtools6, libdatrie0, libdb2, libdb4.4, libdb4.5, libdb4.6, libdbi-perl, libdbus-1-3, libdbus-glib-1-2, libdc1394-13, libdebian-installer4, libdevel-symdump-perl, libdigest-hmac-perl, libdigest-sha1-perl, libdirectfb-1.0-0, libdirectfb-extra, libdjvulibre15, libdmx1, libdrm2, libeb12, libedataserver1.2-9, libedit2, libelfg0, libept0, liberror-perl, libestools1.2, libetoken, libexempi3, libfaad0, libffcall1, libffi5, libfile-ncopy-perl, libfile-remove-perl, libfont-afm-perl, libfontenc1, libforms1, libfreezethaw-perl, libfs6, libfsplib0, libg2-dev, libg20, libg2c0, libgalago3, libgcj-common, libgcj4, libgcr410, libgd2-noxpm, libgdk-pixbuf2, libgdome2-0, libgdome2-cpp-smart0c2a, libgecko2.0-cil, libgfortran3, libggz2, libgif4, libgl1-mesa-glide3, libglew1, libglib-perl, libglib2.0-cil, libglide3, libglu1-mesa, libgmime2.1, libgmp3, libgnome2-vfs-perl, libgnome32, libgnomeprint-bin, libgnomeprint-data, libgnomeprint15, libgnomesupport0, libgnomeui32, libgnorba27, libgnorbagtk0, libgnustep-base1.10, libgnustep-gui0.9, libgnutls26, libgpgme6, libgs8, libgsasl7, libgsf-1-114, libgsf-1-common, libgsmme1c2a, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtk-vnc-1.0-0, libgtk2-perl, libgtk2.0-cil, 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, libio-compress-base-perl, libio-socket-inet6-perl, libio-string-perl, libio-zlib-perl, libiptcdata0, libjaxp1.2-java, libjaxp1.3-java, libkeyutils1, libktoblzcheck1c2a, liblapack3gf, liblazy1, libldap-2.4-2, liblockdev1, liblog4j1.2-java, libloudmouth1-0, liblua5.1-0, liblzo2-2, libmail-sendmail-perl, libmail-spf-query-perl, libmalaga7, libmcrypt4, libmcs1, libmdbtools, libmeanwhile1, libmhash2, libmikmod2, libmoe1.5, libmono-cairo1.0-cil, libmono-corlib1.0-cil, libmono-i18n1.0-cil, libmono-system1.0-cil, libmowgli1, libmozjs0d, libmpcdec3, libmtp7, libmusicbrainz4c2a, libmx4j-java, libncursesw5, libneon25, libneon26, libnet-cidr-lite-perl, libnet-daemon-perl, libnet-dns-perl, libnet-ip-perl, libnet-ph-perl, libnet-snpp-perl, libnet-ssleay-perl, libnet-telnet-perl, libnettle2, libnewt0.52, libnl1, libnotify1, libnspr4-0d, libnss3-0d, libnss3-1d, libntlm0, libobjc1, libobject-realize-later-perl, liboil0.3, libonig2, libopenal0, libopenal1, libopensync0, liborbit0, libparse-recdescent-perl, libpcap0.8, libpci3, libpixman-1-0, libpkcs11-helper1, libplot2c2, libplrpc-perl, libpoppler-glib3, libpoppler3, libpopplerkit0, libportaudio0, libpq4, libraw1394-8, libregexp-java, librplay3, libruby1.6, libsablot0c102, libsasl2-2, libsasl2-modules, libserf-0-0, libservlet2.3-java, libservlet2.4-java, libsieve2-1, libsilc-1.1-2, libslang2, libslbreflex2, libsmpeg0, libsocket6-perl, libsoup2.4-1, libsplashy1, libsqlite3-0, libssh2-1, libssl0.9.8, libstdc++6, 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, libversion-perl, libvoikko1, libvte9, libwpd-stream8c2a, libwpd8c2a, libwpg-0.1-1, libwps-0.1-1, libx11-data, libxapian15, libxau6, libxcb-render-util0, libxcb-render0, libxcb-xlib0, libxcb1, libxcomposite1, libxdamage1, libxdelta2, libxdmcp6, 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, linux-libc-dev, lp-solve, lprng, lsb-base, lsb-release, lsof, lwm, lxsession-lite, lxterminal, lynx-cur, lzma, make, miscfiles, mono-common, mono-jit, mozilla-firefox, mozilla-firefox-locale-nb, mozilla-thunderbird, mpc, myspell-fa, myspell-hr, myspell-hy, myspell-ku, myspell-pt-br, myspell-sk, ncurses-term, netcat-openbsd, netrik, nginx, ocrad, openbox, openssl, openssl-blacklist, openvpn-blacklist, oroborus, pcscd, perl-doc, pm-utils, postgresql-client-7.4, postgresql-client-common, preview-latex-style, psfontmgr, pterm, pwm, python-4suite-doc, python-cups, python-fpconst, python-gdata, python-gobject, python-libxml2, python-minimal, python-support, python2.5, python2.5-minimal, qvwm, ratpoison, rdesktop, readline-common, refblas3, rlpr, robotfindskitten, rox-filer, roxterm, rsyslog, sapphire, sg3-utils, sodipodi, ssl-cert, ssmtp, swfdec-gnome, swfdec-mozilla, tcl8.0, tcl8.5, telepathy-gabble, terminal, thy, timezoneconf, tk8.5, trayer, tsclient, ttf-freefont, ttf-liberation, twm, tzdata, ucspi-unix, unzoo, virtualbox-ose-guest-utils, vtwm, w3c-dtd-xhtml, w9wm, wdg-html-reference, wgerman-medical, windowlab, wm2, wmii, x11-apps, x11-common, x11-session-utils, x11-utils, x11-xfs-utils, x11-xkb-utils, x11-xserver-utils, x11proto-core-dev, x11proto-print-dev, xauth, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-utils, xinit, xkb-data-legacy, xprint-utils, xsltproc, xterm, xutils-dev, yaird, ytalk]
# starts		: 321
# conflicts		: 622307
# decisions		: 1247557
# propagations		: 54671254
# inspects		: 278857635
# shortcuts		: 0
# learnt literals	: 10
# learnt binary clauses	: 76
# learnt ternary clauses	: 25
# learnt constraints	: 622297
# ignored constraints	: 0
# root simplifications	: 0
# removed literals (reason simplification)	: 1929667
# reason swapping (by a shorter reason)	: 0
# Calls to reduceDB	: 31
# Number of update (reduction) of LBD	: 15984
# 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)	: 191822.9038381244
# non guided choices	95440
# learnt constraints type 
# org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 76
# org.sat4j.minisat.constraints.cnf.LearntWLClause => 36138
# Solving done (290.777s).
# WARNING: The solution found MIGHT NOT BE optimal
# Solution contains:861