# Solver launched on Mon Sep 03 09:22:26 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/slowlink/upgrade/easy/rand583.cudf.result
# Objective function -sum(changed,installedsize),-count(removed),-notuptodate(solution),-count(changed)
# 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:5436
# Parsing done (5.451s).
# Solving ...
# Request size: 1012
# Number of  packages after slice: 5183
# Slice efficiency: 91%
# --- Begin Solver configuration ---
# org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@5a5e5a50
# 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:-sum(changed,installedsize),-count(removed),-notuptodate(solution),-count(changed)
# criteria sum(changed,installedsize) size is 0
# criteria removed size is 950 using new vars 6134 to 7084
Skipping unknown criteria:-notuptodate()
# criteria notuptodate() size is 950 using new vars 7084 to 7084
# criteria changed size is 5182 using new vars 7084 to 7084
# p cnf 7083 46089
# Found optimal criterion number 1
# Current objective function value: 24(0.463s)
# Current objective function value: 24(0.594s)
# Current objective function value: 23(0.715s)
# Found optimal criterion number 2
# Current objective function value: 23(0.769s)
# Found optimal criterion number 3
# Current objective function value: 87(0.999s)
# Current objective function value: 85(1.148s)
# Found optimal solution for the last criterion 
# -sum(changed,installedsize) criteria value: 0
# -removed criteria value: 23
# Removed packages: [evolution, gnome, gnome-office, gnumeric, gtkhtml3.2, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdebase, kdenetwork, kdesdk, klipper, kmtrace, kppp, less, libgtkhtml3.2-11, mailx, ppp, pppconfig, pppoe, pppoeconf]
# -changed criteria value: 85
# Changed packages: [-evolution 11090, -fontconfig 11990, fontconfig 12253, fontconfig-config 12253, gcc-4.1-base 15475, -gnome 17322, -gnome-office 17322, -gnumeric 8507, -gnumeric-common 8507, gnumeric-common 9040, -gtkhtml3.2 14458, -kde 20441, -kde-amusements 20441, -kde-core 20441, -kde-devel 20441, -kde-devel-extras 20442, -kdebase 20297, -kdenetwork 20306, -kdesdk 20301, -klipper 20297, -kmtrace 20301, -kppp 20306, larswm 16878, -less 17420, -libc6 12041, libc6 12096, -libc6-dev 12041, libc6-dev 12096, libcairo2 7741, libcairo2-dev 7741, -libfontconfig1 11990, libfontconfig1 12253, -libfontconfig1-dev 11990, libfontconfig1-dev 12253, -libfreetype6 11530, libfreetype6 11738, -libfreetype6-dev 11530, libfreetype6-dev 11738, libg2-dev 5298, libg20 5298, -libgcc1 19603, libgcc1 19690, -libgcrypt11 7605, libgcrypt11 7718, -libgcrypt11-dev 7605, libgcrypt11-dev 7718, libgd2-noxpm 11269, -libglib2.0-0 12633, libglib2.0-0 13307, -libglib2.0-dev 12633, libglib2.0-dev 13307, -libgpg-error-dev 6264, libgpg-error-dev 8337, -libgpg-error0 6264, libgpg-error0 8337, libgsf-1-114 9872, libgsf-1-common 9872, -libgtkhtml3.2-11 14458, -libpango1.0-0 9332, libpango1.0-0 9885, -libpango1.0-common 9332, libpango1.0-common 10056, -libpango1.0-dev 9332, libpango1.0-dev 9885, -libpng12-0 7841, libpng12-0 7919, -libpng12-dev 7841, libpng12-dev 7919, libstdc++6 15475, libwpd-stream8c2a 3197, -libxml2 12701, libxml2 12830, -libxml2-dev 12701, libxml2-dev 12830, -libxslt1.1 7363, libxslt1.1 7400, -mailx 19837, mozilla-firefox 6681, mozilla-firefox-locale-nb 6264, -ppp 12284, -pppconfig 12113, -pppoe 14706, -pppoeconf 9132, robotfindskitten 10770, tzdata 17611]
# starts		: 6
# conflicts		: 504
# decisions		: 21449
# propagations		: 314571
# inspects		: 1117230
# shortcuts		: 0
# learnt literals	: 13
# learnt binary clauses	: 23
# learnt ternary clauses	: 11
# learnt constraints	: 489
# ignored constraints	: 0
# root simplifications	: 0
# removed literals (reason simplification)	: 9083
# reason swapping (by a shorter reason)	: 0
# Calls to reduceDB	: 0
# Number of update (reduction) of LBD	: 19
# 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)	: 217545.64315352697
# non guided choices	15049
# learnt constraints type 
# Solving done (5.122s).
# The solution found IS optimal
# Solution contains:943