# Solver launched on Mon Sep 03 06:40:04 UTC 2012
# Using input file /home/competition/data/upgrade/difficult/rand293.cudf
# Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/difficult/rand293.cudf.result
# Objective function -count(removed),-sum(solution,installedsize),-notuptodate(solution),-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:6873
# Parsing done (6.879s).
# Solving ...
# Request size: 1027
# Number of  packages after slice: 13266
# Slice efficiency: 85%
# --- Begin Solver configuration ---
# org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@fee4648
# 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:-count(removed),-sum(solution,installedsize),-notuptodate(solution),-unsat_recommends(solution),-count(new)
# criteria removed size is 950 using new vars 18162 to 19112
# criteria sum(installedsize) size is 0
Skipping unknown criteria:-notuptodate()
# criteria notuptodate() size is 0 using new vars 19112 to 19112
Skipping unknown criteria:-unsat_recommends()
# criteria unsat_recommends() size is 0 using new vars 19112 to 19112
# criteria new size is 4417 using new vars 19112 to 23529
# p cnf 23528 122856
# Current objective function value: 30(0.991s)
# Current objective function value: 29(1.277s)
# Current objective function value: 21(1.559s)
# Found optimal criterion number 1
# Found optimal criterion number 2
# Current objective function value: 0(1.616s)
# Found optimal criterion number 3
# Current objective function value: 0(1.97s)
# Found optimal criterion number 4
# Current objective function value: 127(2.197s)
# Current objective function value: 71(2.449s)
# Current objective function value: 69(2.815s)
# Current objective function value: 68(2.886s)
# Found optimal solution for the last criterion 
# -removed criteria value: 21
# Removed packages: [gdm, kde, kde-amusements, kde-devel, kde-devel-extras, kdebase-dev, kdegames, kdelibs4-dev, kdenetwork, kdesdk, kspy, ktron, kwifimanager, libarts1-dev, libcroco3-dev, libkonq4-dev, liblablgtk2-ocaml-dev, libqt3-mt-dev, librsvg2-dev, linux-kernel-headers, xlibs-static-dev]
# -sum(installedsize) criteria value: 0
# -new criteria value: 68
# Newly installed packages: [collectd, fontconfig-config, fotoxx, gcc-4.4-base, gmerlin-data, libavahi-client3, libavahi-common-data, libavahi-common3, libc-bin, libc-dev-bin, libcairo2, libcairo2-dev, libcups2, libdatrie1, libdbus-1-3, libgda-4.0-doc, libgnutls26, libgssapi-krb5-2, libjasper1, libk5crypto3, libkeyutils1, libkrb5-3, libkrb5support0, libpcrecpp0, libpixman-1-0, libpixman-1-dev, libpthread-stubs0, libpthread-stubs0-dev, librrd4, libstdc++6, libtasn1-3, libthai-data, libthai0, libx11-data, libxau-dev, libxau6, libxcb-render-util0, libxcb-render-util0-dev, libxcb-render0, libxcb-render0-dev, libxcb1, libxcb1-dev, libxcomposite-dev, libxcomposite1, libxdamage-dev, libxdamage1, libxdmcp-dev, libxdmcp6, libxfixes-dev, libxfixes3, libxinerama-dev, libxinerama1, linux-libc-dev, lsb-base, ttf-mona, x11-common, x11proto-composite-dev, x11proto-core-dev, x11proto-damage-dev, x11proto-fixes-dev, x11proto-input-dev, x11proto-kb-dev, x11proto-randr-dev, x11proto-xext-dev, x11proto-xinerama-dev, xbitmaps, xcursor-themes, xtrans-dev]
# starts		: 10
# conflicts		: 612
# decisions		: 495978
# propagations		: 3174023
# inspects		: 8751211
# shortcuts		: 0
# learnt literals	: 79
# learnt binary clauses	: 250
# learnt ternary clauses	: 69
# learnt constraints	: 531
# ignored constraints	: 0
# root simplifications	: 0
# removed literals (reason simplification)	: 100
# reason swapping (by a shorter reason)	: 0
# Calls to reduceDB	: 0
# Number of update (reduction) of LBD	: 90
# 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)	: 1097897.9591836734
# non guided choices	368689
# learnt constraints type 
# Solving done (7.171s).
# The solution found IS optimal
# Solution contains:997