# Solver launched on Mon Sep 03 06:35:18 UTC 2012
# Using input file /home/competition/data/upgrade/easy/rand268.cudf
# Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/easy/rand268.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:5434
# Parsing done (5.44s).
# Solving ...
# Request size: 1012
# Number of  packages after slice: 8174
# Slice efficiency: 85%
# --- Begin Solver configuration ---
# org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@63b9240e
# 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 11393 to 12343
# criteria sum(installedsize) size is 0
Skipping unknown criteria:-notuptodate()
# criteria notuptodate() size is 0 using new vars 12343 to 12343
Skipping unknown criteria:-unsat_recommends()
# criteria unsat_recommends() size is 0 using new vars 12343 to 12343
# criteria new size is 2985 using new vars 12343 to 15328
# p cnf 15327 75268
# Current objective function value: 47(1.013s)
# Current objective function value: 46(1.387s)
# Current objective function value: 40(1.536s)
# Found optimal criterion number 1
# Found optimal criterion number 2
# Current objective function value: 0(1.567s)
# Found optimal criterion number 3
# Current objective function value: 0(1.731s)
# Found optimal criterion number 4
# Current objective function value: 63(1.858s)
# Current objective function value: 47(1.978s)
# Current objective function value: 46(2.171s)
# Current objective function value: 45(2.28s)
# Current objective function value: 32(2.338s)
# Found optimal solution for the last criterion 
# -removed criteria value: 40
# Removed packages: [capplets, enscript, gdm, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-games, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, gnome-themes-extras, gnome-volume-manager, gstreamer0.8-plugin-apps, gstreamer0.8-tools, gtk2-engines-spherecrystal, hal, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdeaddons, kdebase, kdeprint, liblablgtk2-ocaml, liblablgtk2-ocaml-dev, libnautilus2-2, librsvg2-2, librsvg2-common, librsvg2-dev, libsvga1, nautilus, nautilus-cd-burner, nautilus-media, noatun-plugins, udev]
# -sum(installedsize) criteria value: 0
# -new criteria value: 32
# Newly installed packages: [comerr-dev, cpp-4.1, gcc-4.1, gcc-4.1-base, gnat-4.1, gnat-4.1-base, h5utils, libgnadeodbc-dev, libgnadeodbc1.6, libgnadepostgresql-dev, libgnadepostgresql1.6, libgnat-4.1, libgnatprj4.1, libgnatvsn4.1, libhdf4g, libhdf5-serial-1.6.2-0, libkadm55, libkrb5-dev, libltdl3, libmatheval1, libpq-dev, libpq4, libssl0.9.8, libssp0, locales-all, odbcinst1debian1, openoffice.org-l10n-ml-in, readline-common, scite, tzdata, unixodbc, xlaby]
# starts		: 11
# conflicts		: 279
# decisions		: 173576
# propagations		: 1061565
# inspects		: 3229716
# shortcuts		: 0
# learnt literals	: 23
# learnt binary clauses	: 105
# learnt ternary clauses	: 21
# learnt constraints	: 254
# ignored constraints	: 0
# root simplifications	: 0
# removed literals (reason simplification)	: 62
# reason swapping (by a shorter reason)	: 0
# Calls to reduceDB	: 0
# Number of update (reduction) of LBD	: 35
# 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)	: 470551.86170212773
# non guided choices	136025
# learnt constraints type 
# Solving done (6.849s).
# The solution found IS optimal
# Solution contains:942