PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-tr12-30.opb
MD5SUM	2d8f46b77d84c45a7178d4a463744176
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	7560
Biggest coefficient in the objective function	2097152
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	876993750
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	2097152
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	876993750
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.128979
Number of variables	14760
Total number of constraints	1110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	360
Number of constraints which are nor clauses,nor cardinality constraints	750
Minimum length of a constraint	1
Maximum length of a constraint	252
Trace number 18955

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 17:19:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18109 boxname=wulflinc25 idbench=1393 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2d8f46b77d84c45a7178d4a463744176  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-tr12-30.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-tr12-30.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-tr12-30.opb
IDLAUNCH: 18109
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        522056 kB
Buffers:         30404 kB
Cached:         461172 kB
SwapCached:        744 kB
Active:          93024 kB
Inactive:       400524 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        521804 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            13324 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:39:23 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 18109 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1108]---> BDD-cost:   71
c ---[1106]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1102]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1100]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1098]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1096]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1094]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1092]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1090]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1088]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1086]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1084]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1082]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1080]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1078]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1076]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1074]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1072]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1070]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1068]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1066]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1064]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1062]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1060]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1058]---> BDD-cost:   52
c ---[1056]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1054]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1052]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1050]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1048]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1046]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1044]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1042]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1040]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1038]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1036]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1034]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1032]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1030]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1028]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1026]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1024]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1022]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1020]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1018]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1016]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1014]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1012]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1010]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1008]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1006]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1004]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1002]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1000]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 998]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 996]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 994]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 992]---> BDD-cost:   65
c ---[ 990]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 988]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 986]---> BDD-cost:  166
c ---[ 984]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 982]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 980]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 978]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 976]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 974]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 972]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 970]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 968]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 966]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 964]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 962]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 960]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 958]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 956]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 950]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 948]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 946]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 944]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 942]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 940]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 938]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 936]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 934]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 932]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 930]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 928]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 926]---> BDD-cost:   67
c ---[ 924]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 922]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 920]---> BDD-cost:  166
c ---[ 918]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 916]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 914]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 912]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 910]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 908]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 906]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 904]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 902]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 900]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 898]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 896]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 894]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 892]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 890]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 888]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 886]---> BDD-cost:  159
c ---[ 884]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 882]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 880]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 878]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 876]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 874]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 872]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 870]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 868]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 866]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 864]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 862]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 860]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 858]---> BDD-cost:   63
c ---[ 856]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 854]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 852]---> BDD-cost:  166
c ---[ 850]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 848]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 846]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 844]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 842]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 840]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 838]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 836]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 834]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 832]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 830]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 828]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 826]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 824]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 822]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 820]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 818]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 816]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 814]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 810]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 808]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 806]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 804]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 802]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 800]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 798]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 796]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 794]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 792]---> BDD-cost:   71
c ---[ 790]---> BDD-cost:  159
c ---[ 788]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 776]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 770]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 740]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 738]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 736]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 732]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 730]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 728]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 726]---> BDD-cost:   52
c ---[ 724]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> BDD-cost:  164
c ---[ 720]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 718]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 716]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 710]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 708]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 702]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 698]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 694]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 692]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 688]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 684]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 680]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 678]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 676]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 670]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 668]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 662]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> BDD-cost:   71
c ---[ 656]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 650]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 648]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 646]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 644]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 640]---> BDD-cost:   67
c ---[ 638]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 636]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 632]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 628]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 622]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 620]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 618]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 614]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 610]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 606]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 602]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 598]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 596]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 594]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> BDD-cost:   52
c ---[ 590]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> BDD-cost:  166
c ---[ 584]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 554]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 552]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 536]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 527]---> BDD-cost:   28
c ---[ 526]---> BDD-cost:   28
c ---[ 525]---> BDD-cost:   28
c ---[ 524]---> BDD-cost:   28
c ---[ 523]---> BDD-cost:   28
c ---[ 522]---> BDD-cost:   28
c ---[ 521]---> BDD-cost:   28
c ---[ 520]---> BDD-cost:   28
c ---[ 519]---> BDD-cost:   28
c ---[ 517]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> BDD-cost:   28
c ---[ 515]---> BDD-cost:   28
c ---[ 514]---> BDD-cost:   28
c ---[ 513]---> BDD-cost:   28
c ---[ 512]---> BDD-cost:   28
c ---[ 511]---> BDD-cost:   28
c ---[ 510]---> BDD-cost:   28
c ---[ 509]---> BDD-cost:   28
c ---[ 508]---> BDD-cost:   28
c ---[ 507]---> BDD-cost:   28
c ---[ 505]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> BDD-cost:   28
c ---[ 503]---> BDD-cost:   28
c ---[ 502]---> BDD-cost:   28
c ---[ 501]---> BDD-cost:   28
c ---[ 500]---> BDD-cost:   28
c ---[ 499]---> BDD-cost:   28
c ---[ 498]---> BDD-cost:   28
c ---[ 497]---> BDD-cost:   28
c ---[ 496]---> BDD-cost:   28
c ---[ 495]---> BDD-cost:   28
c ---[ 493]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> BDD-cost:   28
c ---[ 491]---> BDD-cost:   27
c ---[ 490]---> BDD-cost:   27
c ---[ 489]---> BDD-cost:   27
c ---[ 488]---> BDD-cost:   27
c ---[ 487]---> BDD-cost:   27
c ---[ 486]---> BDD-cost:   27
c ---[ 485]---> BDD-cost:   27
c ---[ 484]---> BDD-cost:   27
c ---[ 483]---> BDD-cost:   27
c ---[ 481]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> BDD-cost:   27
c ---[ 477]---> BDD-cost:   27
c ---[ 476]---> BDD-cost:   27
c ---[ 475]---> BDD-cost:   27
c ---[ 474]---> BDD-cost:   27
c ---[ 473]---> BDD-cost:   27
c ---[ 472]---> BDD-cost:   27
c ---[ 471]---> BDD-cost:   27
c ---[ 470]---> BDD-cost:   27
c ---[ 469]---> BDD-cost:   27
c ---[ 467]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> BDD-cost:   27
c ---[ 465]---> BDD-cost:   27
c ---[ 464]---> BDD-cost:   27
c ---[ 463]---> BDD-cost:   27
c ---[ 462]---> BDD-cost:   27
c ---[ 461]---> BDD-cost:   27
c ---[ 460]---> BDD-cost:   27
c ---[ 459]---> BDD-cost:   27
c ---[ 458]---> BDD-cost:   27
c ---[ 457]---> BDD-cost:   27
c ---[ 455]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> BDD-cost:   27
c ---[ 453]---> BDD-cost:   25
c ---[ 452]---> BDD-cost:   25
c ---[ 451]---> BDD-cost:   25
c ---[ 450]---> BDD-cost:   25
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> BDD-cost:   25
c ---[ 447]---> BDD-cost:   25
c ---[ 446]---> BDD-cost:   25
c ---[ 445]---> BDD-cost:   25
c ---[ 443]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> BDD-cost:   25
c ---[ 441]---> BDD-cost:   25
c ---[ 440]---> BDD-cost:   25
c ---[ 439]---> BDD-cost:   25
c ---[ 438]---> BDD-cost:   25
c ---[ 437]---> BDD-cost:   25
c ---[ 436]---> BDD-cost:   25
c ---[ 435]---> BDD-cost:   25
c ---[ 434]---> BDD-cost:   25
c ---[ 433]---> BDD-cost:   25
c ---[ 431]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> BDD-cost:   25
c ---[ 429]---> BDD-cost:   25
c ---[ 428]---> BDD-cost:   25
c ---[ 427]---> BDD-cost:   25
c ---[ 426]---> BDD-cost:   25
c ---[ 425]---> BDD-cost:   25
c ---[ 424]---> BDD-cost:   25
c ---[ 423]---> BDD-cost:   25
c ---[ 422]---> BDD-cost:   25
c ---[ 421]---> BDD-cost:   25
c ---[ 419]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> BDD-cost:   25
c ---[ 417]---> BDD-cost:   28
c ---[ 416]---> BDD-cost:   28
c ---[ 415]---> BDD-cost:   28
c ---[ 414]---> BDD-cost:   28
c ---[ 413]---> BDD-cost:   28
c ---[ 412]---> BDD-cost:   28
c ---[ 411]---> BDD-cost:   28
c ---[ 410]---> BDD-cost:   28
c ---[ 409]---> BDD-cost:   28
c ---[ 407]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> BDD-cost:   28
c ---[ 405]---> BDD-cost:   28
c ---[ 404]---> BDD-cost:   28
c ---[ 403]---> BDD-cost:   28
c ---[ 402]---> BDD-cost:   28
c ---[ 401]---> BDD-cost:   28
c ---[ 400]---> BDD-cost:   28
c ---[ 399]---> BDD-cost:   28
c ---[ 398]---> BDD-cost:   28
c ---[ 397]---> BDD-cost:   28
c ---[ 395]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> BDD-cost:   28
c ---[ 393]---> BDD-cost:   28
c ---[ 392]---> BDD-cost:   28
c ---[ 391]---> BDD-cost:   28
c ---[ 390]---> BDD-cost:   28
c ---[ 389]---> BDD-cost:   28
c ---[ 388]---> BDD-cost:   28
c ---[ 387]---> BDD-cost:   28
c ---[ 386]---> BDD-cost:   28
c ---[ 385]---> BDD-cost:   28
c ---[ 383]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> BDD-cost:   28
c ---[ 381]---> BDD-cost:   28
c ---[ 380]---> BDD-cost:   28
c ---[ 379]---> BDD-cost:   28
c ---[ 378]---> BDD-cost:   28
c ---[ 377]---> BDD-cost:   28
c ---[ 376]---> BDD-cost:   28
c ---[ 375]---> BDD-cost:   28
c ---[ 374]---> BDD-cost:   28
c ---[ 373]---> BDD-cost:   28
c ---[ 371]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> BDD-cost:   28
c ---[ 369]---> BDD-cost:   28
c ---[ 368]---> BDD-cost:   28
c ---[ 367]---> BDD-cost:   28
c ---[ 366]---> BDD-cost:   28
c ---[ 365]---> BDD-cost:   28
c ---[ 364]---> BDD-cost:   28
c ---[ 363]---> BDD-cost:   28
c ---[ 362]---> BDD-cost:   28
c ---[ 361]---> BDD-cost:   28
c ---[ 359]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 357]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> BDD-cost:   28
c ---[ 355]---> BDD-cost:   28
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:   28
c ---[ 352]---> BDD-cost:   28
c ---[ 351]---> BDD-cost:   28
c ---[ 350]---> BDD-cost:   28
c ---[ 349]---> BDD-cost:   28
c ---[ 348]---> BDD-cost:   28
c ---[ 347]---> BDD-cost:   28
c ---[ 345]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> BDD-cost:   28
c ---[ 343]---> BDD-cost:   28
c ---[ 342]---> BDD-cost:   28
c ---[ 341]---> BDD-cost:   28
c ---[ 340]---> BDD-cost:   28
c ---[ 339]---> BDD-cost:   28
c ---[ 338]---> BDD-cost:   28
c ---[ 337]---> BDD-cost:   28
c ---[ 336]---> BDD-cost:   28
c ---[ 335]---> BDD-cost:   28
c ---[ 333]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:   28
c ---[ 331]---> BDD-cost:   28
c ---[ 330]---> BDD-cost:   28
c ---[ 329]---> BDD-cost:   28
c ---[ 328]---> BDD-cost:   28
c ---[ 327]---> BDD-cost:   28
c ---[ 326]---> BDD-cost:   28
c ---[ 325]---> BDD-cost:   28
c ---[ 324]---> BDD-cost:   28
c ---[ 323]---> BDD-cost:   28
c ---[ 321]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> BDD-cost:   28
c ---[ 319]---> BDD-cost:   28
c ---[ 318]---> BDD-cost:   28
c ---[ 317]---> BDD-cost:   28
c ---[ 316]---> BDD-cost:   28
c ---[ 315]---> BDD-cost:   28
c ---[ 314]---> BDD-cost:   28
c ---[ 313]---> BDD-cost:   28
c ---[ 312]---> BDD-cost:   28
c ---[ 311]---> BDD-cost:   28
c ---[ 309]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> BDD-cost:   28
c ---[ 307]---> BDD-cost:   27
c ---[ 306]---> BDD-cost:   27
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   27
c ---[ 303]---> BDD-cost:   27
c ---[ 302]---> BDD-cost:   27
c ---[ 301]---> BDD-cost:   27
c ---[ 300]---> BDD-cost:   27
c ---[ 299]---> BDD-cost:   27
c ---[ 297]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> BDD-cost:   27
c ---[ 295]---> BDD-cost:   27
c ---[ 294]---> BDD-cost:   27
c ---[ 293]---> BDD-cost:   27
c ---[ 292]---> BDD-cost:   27
c ---[ 291]---> BDD-cost:   27
c ---[ 290]---> BDD-cost:   27
c ---[ 289]---> BDD-cost:   27
c ---[ 288]---> BDD-cost:   27
c ---[ 287]---> BDD-cost:   27
c ---[ 285]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> BDD-cost:   27
c ---[ 283]---> BDD-cost:   27
c ---[ 282]---> BDD-cost:   27
c ---[ 281]---> BDD-cost:   27
c ---[ 280]---> BDD-cost:   27
c ---[ 279]---> BDD-cost:   27
c ---[ 278]---> BDD-cost:   27
c ---[ 277]---> BDD-cost:   27
c ---[ 276]---> BDD-cost:   27
c ---[ 275]---> BDD-cost:   27
c ---[ 273]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> BDD-cost:   27
c ---[ 271]---> BDD-cost:   27
c ---[ 270]---> BDD-cost:   27
c ---[ 269]---> BDD-cost:   27
c ---[ 268]---> BDD-cost:   27
c ---[ 267]---> BDD-cost:   27
c ---[ 266]---> BDD-cost:   27
c ---[ 265]---> BDD-cost:   27
c ---[ 264]---> BDD-cost:   27
c ---[ 263]---> BDD-cost:   27
c ---[ 261]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 260]---> BDD-cost:   27
c ---[ 259]---> BDD-cost:   27
c ---[ 258]---> BDD-cost:   27
c ---[ 257]---> BDD-cost:   27
c ---[ 256]---> BDD-cost:   27
c ---[ 255]---> BDD-cost:   27
c ---[ 254]---> BDD-cost:   27
c ---[ 253]---> BDD-cost:   27
c ---[ 252]---> BDD-cost:   27
c ---[ 251]---> BDD-cost:   27
c ---[ 249]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 248]---> BDD-cost:   27
c ---[ 247]---> BDD-cost:   27
c ---[ 246]---> BDD-cost:   27
c ---[ 245]---> BDD-cost:   27
c ---[ 244]---> BDD-cost:   27
c ---[ 243]---> BDD-cost:   27
c ---[ 242]---> BDD-cost:   27
c ---[ 241]---> BDD-cost:   27
c ---[ 240]---> BDD-cost:   27
c ---[ 239]---> BDD-cost:   27
c ---[ 237]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 234]---> BDD-cost:   27
c ---[ 233]---> BDD-cost:   28
c ---[ 232]---> BDD-cost:   28
c ---[ 231]---> BDD-cost:   28
c ---[ 230]---> BDD-cost:   28
c ---[ 229]---> BDD-cost:   28
c ---[ 228]---> BDD-cost:   28
c ---[ 227]---> BDD-cost:   28
c ---[ 226]---> BDD-cost:   28
c ---[ 225]---> BDD-cost:   28
c ---[ 223]---> BDD-cost:   52
c ---[ 222]---> BDD-cost:   28
c ---[ 221]---> BDD-cost:   28
c ---[ 220]---> BDD-cost:   28
c ---[ 219]---> BDD-cost:   28
c ---[ 218]---> BDD-cost:   28
c ---[ 217]---> BDD-cost:   28
c ---[ 216]---> BDD-cost:   28
c ---[ 215]---> BDD-cost:   28
c ---[ 214]---> BDD-cost:   28
c ---[ 213]---> BDD-cost:   28
c ---[ 211]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 210]---> BDD-cost:   28
c ---[ 209]---> BDD-cost:   28
c ---[ 208]---> BDD-cost:   28
c ---[ 207]---> BDD-cost:   28
c ---[ 206]---> BDD-cost:   28
c ---[ 205]---> BDD-cost:   28
c ---[ 204]---> BDD-cost:   28
c ---[ 203]---> BDD-cost:   28
c ---[ 202]---> BDD-cost:   28
c ---[ 201]---> BDD-cost:   28
c ---[ 199]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   25
c ---[ 196]---> BDD-cost:   25
c ---[ 195]---> BDD-cost:   25
c ---[ 194]---> BDD-cost:   25
c ---[ 193]---> BDD-cost:   25
c ---[ 192]---> BDD-cost:   25
c ---[ 191]---> BDD-cost:   25
c ---[ 190]---> BDD-cost:   25
c ---[ 189]---> BDD-cost:   25
c ---[ 187]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> BDD-cost:   25
c ---[ 185]---> BDD-cost:   25
c ---[ 184]---> BDD-cost:   25
c ---[ 183]---> BDD-cost:   25
c ---[ 182]---> BDD-cost:   25
c ---[ 181]---> BDD-cost:   25
c ---[ 180]---> BDD-cost:   25
c ---[ 179]---> BDD-cost:   25
c ---[ 178]---> BDD-cost:   25
c ---[ 177]---> BDD-cost:   25
c ---[ 175]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> BDD-cost:   25
c ---[ 173]---> BDD-cost:   25
c ---[ 172]---> BDD-cost:   25
c ---[ 171]---> BDD-cost:   25
c ---[ 170]---> BDD-cost:   25
c ---[ 169]---> BDD-cost:   25
c ---[ 168]---> BDD-cost:   25
c ---[ 167]---> BDD-cost:   25
c ---[ 166]---> BDD-cost:   25
c ---[ 165]---> BDD-cost:   25
c ---[ 163]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> BDD-cost:   25
c ---[ 161]---> BDD-cost:   27
c ---[ 160]---> BDD-cost:   27
c ---[ 159]---> BDD-cost:   27
c ---[ 158]---> BDD-cost:   27
c ---[ 157]---> BDD-cost:   27
c ---[ 156]---> BDD-cost:   27
c ---[ 155]---> BDD-cost:   27
c ---[ 154]---> BDD-cost:   27
c ---[ 153]---> BDD-cost:   27
c ---[ 151]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> BDD-cost:   27
c ---[ 149]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   27
c ---[ 147]---> BDD-cost:   27
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   27
c ---[ 144]---> BDD-cost:   27
c ---[ 143]---> BDD-cost:   27
c ---[ 142]---> BDD-cost:   27
c ---[ 141]---> BDD-cost:   27
c ---[ 139]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> BDD-cost:   27
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   27
c ---[ 131]---> BDD-cost:   27
c ---[ 130]---> BDD-cost:   27
c ---[ 129]---> BDD-cost:   27
c ---[ 127]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   25
c ---[ 124]---> BDD-cost:   25
c ---[ 123]---> BDD-cost:   25
c ---[ 122]---> BDD-cost:   25
c ---[ 121]---> BDD-cost:   25
c ---[ 120]---> BDD-cost:   25
c ---[ 119]---> BDD-cost:   25
c ---[ 118]---> BDD-cost:   25
c ---[ 117]---> BDD-cost:   25
c ---[ 115]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:   25
c ---[ 111]---> BDD-cost:   25
c ---[ 110]---> BDD-cost:   25
c ---[ 109]---> BDD-cost:   25
c ---[ 108]---> BDD-cost:   25
c ---[ 107]---> BDD-cost:   25
c ---[ 106]---> BDD-cost:   25
c ---[ 105]---> BDD-cost:   25
c ---[ 104]---> BDD-cost:   25
c ---[ 103]---> BDD-cost:   25
c ---[ 101]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> BDD-cost:   25
c ---[  99]---> BDD-cost:   25
c ---[  98]---> BDD-cost:   25
c ---[  97]---> BDD-cost:   25
c ---[  96]---> BDD-cost:   25
c ---[  95]---> BDD-cost:   25
c ---[  94]---> BDD-cost:   25
c ---[  93]---> BDD-cost:   25
c ---[  92]---> BDD-cost:   25
c ---[  91]---> BDD-cost:   25
c ---[  89]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> BDD-cost:   25
c ---[  87]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  86]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  85]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  84]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  83]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  82]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  81]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  80]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  79]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  77]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  76]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  75]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  74]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  73]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  72]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  71]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  70]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  69]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  68]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  67]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  65]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  63]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  62]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  61]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  60]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  59]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  58]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  57]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  56]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  55]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  50]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> BDD-cost:   71
c ---[  14]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> BDD-cost:  164
c ---[  10]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  466205  1229635 |  155401       0        0     nan |  0.000 % |
c |       100 |  465872  1228888 |  170941      55      175     3.2 | 11.176 % |
c |       250 |  465172  1227326 |  188035     122      405     3.3 | 11.304 % |
c |       475 |  464333  1225457 |  206838     246      773     3.1 | 11.451 % |
c |       812 |  463090  1222667 |  227522     445     1394     3.1 | 11.670 % |
c |      1320 |  461897  1219980 |  250274     821     2850     3.5 | 11.881 % |
c |      2079 |  460881  1217640 |  275302    1453     5408     3.7 | 12.056 % |
c |      3218 |  460123  1215868 |  302832    2490     9806     3.9 | 12.184 % |
c |      4926 |  458397  1211872 |  333115    3981    16249     4.1 | 12.482 % |
c |      7489 |  457348  1209271 |  366427    6416    46635     7.3 | 12.636 % |
c |     11333 |  456813  1207987 |  403070   10142   116744    11.5 | 12.727 % |
c |     17099 |  454623  1203033 |  443377   15553   208408    13.4 | 13.112 % |
c |     25748 |  451825  1196671 |  487714   23852   366077    15.3 | 13.602 % |
c |     38724 |  451771  1196489 |  536486   36817   694305    18.9 | 13.608 % |
c |     58185 |  451762  1196458 |  590135   56270  1820582    32.4 | 13.608 % |
c |     87381 |  451624  1196146 |  649148   85447  2633203    30.8 | 13.633 % |
c |    131170 |  451544  1195964 |  714063  129228  3737007    28.9 | 13.647 % |
c |    196854 |  451346  1195481 |  785469  194889  5906315    30.3 | 13.678 % |
c |    295385 |  451155  1195013 |  864016  293223  9432360    32.2 | 13.708 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.72 0.92 0.97 2/54 9761
Raw data (stat): 9761 (runsolver) R 9760 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546837261 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99996 s]
Raw data (loadavg): 0.76 0.92 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14317 0 0 0 964 35 0 0 25 0 1 0 546837261 67612672 13569 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16507 13569 603 41 0 16466 0
vsize: 66028
[startup+20.0005 s]
Raw data (loadavg): 0.80 0.93 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14317 0 0 0 1964 35 0 0 25 0 1 0 546837261 67612672 13569 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16507 13569 603 41 0 16466 0
vsize: 66028
[startup+30.0011 s]
Raw data (loadavg): 0.83 0.93 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14319 0 0 0 2963 35 0 0 25 0 1 0 546837261 67612672 13571 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16507 13571 603 41 0 16466 0
vsize: 66028
[startup+40.0007 s]
Raw data (loadavg): 0.85 0.93 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14321 0 0 0 3963 36 0 0 25 0 1 0 546837261 67612672 13573 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16507 13573 603 41 0 16466 0
vsize: 66028
[startup+50.0014 s]
Raw data (loadavg): 0.88 0.93 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14321 0 0 0 4963 36 0 0 25 0 1 0 546837261 67612672 13573 4294967295 134512640 134672761 3221224544 3221223712 134564732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16507 13573 603 41 0 16466 0
vsize: 66028
[startup+60.0009 s]
Raw data (loadavg): 0.89 0.93 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14329 0 0 0 5963 36 0 0 25 0 1 0 546837261 67612672 13581 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16507 13581 603 41 0 16466 0
vsize: 66028
[startup+70.0015 s]
Raw data (loadavg): 0.91 0.93 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14376 0 0 0 6963 37 0 0 25 0 1 0 546837261 67747840 13628 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16540 13628 603 41 0 16499 0
vsize: 66160
[startup+80.0021 s]
Raw data (loadavg): 0.92 0.94 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14412 0 0 0 7962 37 0 0 25 0 1 0 546837261 67883008 13664 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16573 13664 603 41 0 16532 0
vsize: 66292
[startup+90.0017 s]
Raw data (loadavg): 0.93 0.94 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14447 0 0 0 8962 37 0 0 25 0 1 0 546837261 68018176 13699 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16606 13699 603 41 0 16565 0
vsize: 66424
[startup+100.001 s]
Raw data (loadavg): 0.94 0.94 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14469 0 0 0 9962 38 0 0 25 0 1 0 546837261 68153344 13721 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16639 13721 603 41 0 16598 0
vsize: 66556
[startup+110.002 s]
Raw data (loadavg): 0.95 0.94 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14480 0 0 0 10962 38 0 0 25 0 1 0 546837261 68153344 13732 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16639 13732 603 41 0 16598 0
vsize: 66556
[startup+120.003 s]
Raw data (loadavg): 0.96 0.94 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14504 0 0 0 11962 38 0 0 25 0 1 0 546837261 68288512 13756 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16672 13756 603 41 0 16631 0
vsize: 66688
[startup+130.002 s]
Raw data (loadavg): 0.97 0.94 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14579 0 0 0 12961 39 0 0 25 0 1 0 546837261 68558848 13831 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16738 13831 603 41 0 16697 0
vsize: 66952
[startup+140.002 s]
Raw data (loadavg): 0.97 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14665 0 0 0 13960 40 0 0 25 0 1 0 546837261 68829184 13917 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16804 13917 603 41 0 16763 0
vsize: 67216
[startup+150.002 s]
Raw data (loadavg): 0.97 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14724 0 0 0 14960 40 0 0 25 0 1 0 546837261 69095424 13976 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16869 13976 603 41 0 16828 0
vsize: 67476
[startup+160.002 s]
Raw data (loadavg): 0.98 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14731 0 0 0 15960 41 0 0 25 0 1 0 546837261 69095424 13983 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16869 13983 603 41 0 16828 0
vsize: 67476
[startup+170.003 s]
Raw data (loadavg): 0.98 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14764 0 0 0 16959 41 0 0 25 0 1 0 546837261 69226496 14016 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16901 14016 603 41 0 16860 0
vsize: 67604
[startup+180.003 s]
Raw data (loadavg): 0.98 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14837 0 0 0 17959 42 0 0 25 0 1 0 546837261 69689344 14089 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17014 14089 603 41 0 16973 0
vsize: 68056
[startup+190.003 s]
Raw data (loadavg): 0.98 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14838 0 0 0 18959 42 0 0 25 0 1 0 546837261 69689344 14090 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17014 14090 603 41 0 16973 0
vsize: 68056
[startup+200.002 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14846 0 0 0 19958 43 0 0 25 0 1 0 546837261 69689344 14098 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17014 14098 603 41 0 16973 0
vsize: 68056
[startup+210.002 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14855 0 0 0 20958 43 0 0 25 0 1 0 546837261 69689344 14107 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17014 14107 603 41 0 16973 0
vsize: 68056
[startup+220.003 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 14892 0 0 0 21958 44 0 0 25 0 1 0 546837261 69820416 14144 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17046 14144 603 41 0 17005 0
vsize: 68184
[startup+230.003 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 15265 0 0 0 22956 45 0 0 25 0 1 0 546837261 71299072 14517 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17407 14517 603 41 0 17366 0
vsize: 69628
[startup+240.003 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 15596 0 0 0 23955 47 0 0 25 0 1 0 546837261 72810496 14848 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17776 14848 603 41 0 17735 0
vsize: 71104
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 16306 0 0 0 24953 49 0 0 25 0 1 0 546837261 75767808 15558 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18498 15558 603 41 0 18457 0
vsize: 73992
[startup+260.003 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 16876 0 0 0 25951 52 0 0 25 0 1 0 546837261 78082048 16128 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19063 16128 603 41 0 19022 0
vsize: 76252
[startup+270.004 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 17134 0 0 0 26951 52 0 0 25 0 1 0 546837261 79020032 16386 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19292 16386 603 41 0 19251 0
vsize: 77168
[startup+280.005 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 17374 0 0 0 27949 53 0 0 25 0 1 0 546837261 80359424 16626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19619 16626 603 41 0 19578 0
vsize: 78476
[startup+290.004 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 17649 0 0 0 28948 55 0 0 25 0 1 0 546837261 81453056 16901 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19886 16901 603 41 0 19845 0
vsize: 79544
[startup+300.004 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 17853 0 0 0 29947 56 0 0 25 0 1 0 546837261 82276352 17105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20087 17105 603 41 0 20046 0
vsize: 80348
[startup+310.004 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 18069 0 0 0 30945 58 0 0 25 0 1 0 546837261 83173376 17321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20306 17321 603 41 0 20265 0
vsize: 81224
[startup+320.005 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 18278 0 0 0 31944 59 0 0 25 0 1 0 546837261 84000768 17530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20508 17530 603 41 0 20467 0
vsize: 82032
[startup+330.004 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 18384 0 0 0 32943 60 0 0 25 0 1 0 546837261 84406272 17636 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20607 17636 603 41 0 20566 0
vsize: 82428
[startup+340.004 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 18524 0 0 0 33943 61 0 0 25 0 1 0 546837261 85196800 17776 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20800 17776 603 41 0 20759 0
vsize: 83200
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 18639 0 0 0 34942 61 0 0 25 0 1 0 546837261 85602304 17891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20899 17891 603 41 0 20858 0
vsize: 83596
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.97 3/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 18758 0 0 0 35942 62 0 0 25 0 1 0 546837261 86020096 18010 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21001 18010 603 41 0 20960 0
vsize: 84004
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 18898 0 0 0 36942 62 0 0 25 0 1 0 546837261 86560768 18150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21133 18150 603 41 0 21092 0
vsize: 84532
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19041 0 0 0 37941 63 0 0 25 0 1 0 546837261 87244800 18293 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21300 18293 603 41 0 21259 0
vsize: 85200
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19160 0 0 0 38940 64 0 0 25 0 1 0 546837261 87683072 18412 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21407 18412 603 41 0 21366 0
vsize: 85628
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19244 0 0 0 39940 64 0 0 25 0 1 0 546837261 88096768 18496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21508 18496 603 41 0 21467 0
vsize: 86032
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19403 0 0 0 40939 65 0 0 25 0 1 0 546837261 88764416 18655 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21671 18655 603 41 0 21630 0
vsize: 86684
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19590 0 0 0 41939 66 0 0 25 0 1 0 546837261 89464832 18842 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21842 18842 603 41 0 21801 0
vsize: 87368
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19683 0 0 0 42939 66 0 0 25 0 1 0 546837261 90451968 18935 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22083 18935 603 41 0 22042 0
vsize: 88332
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19785 0 0 0 43938 67 0 0 25 0 1 0 546837261 90890240 19037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22190 19037 603 41 0 22149 0
vsize: 88760
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19884 0 0 0 44937 68 0 0 25 0 1 0 546837261 91377664 19136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22309 19136 603 41 0 22268 0
vsize: 89236
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 19992 0 0 0 45937 68 0 0 25 0 1 0 546837261 91865088 19244 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22428 19244 603 41 0 22387 0
vsize: 89712
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20105 0 0 0 46937 69 0 0 25 0 1 0 546837261 92262400 19357 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22525 19357 603 41 0 22484 0
vsize: 90100
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20216 0 0 0 47936 69 0 0 25 0 1 0 546837261 92839936 19468 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22666 19468 603 41 0 22625 0
vsize: 90664
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20281 0 0 0 48936 69 0 0 25 0 1 0 546837261 93061120 19533 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22720 19533 603 41 0 22679 0
vsize: 90880
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20371 0 0 0 49935 71 0 0 25 0 1 0 546837261 93454336 19623 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22816 19623 603 41 0 22775 0
vsize: 91264
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20449 0 0 0 50935 71 0 0 25 0 1 0 546837261 93843456 19701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22911 19701 603 41 0 22870 0
vsize: 91644
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20547 0 0 0 51935 71 0 0 25 0 1 0 546837261 94289920 19799 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23020 19799 603 41 0 22979 0
vsize: 92080
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20653 0 0 0 52934 73 0 0 25 0 1 0 546837261 94703616 19905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23121 19905 603 41 0 23080 0
vsize: 92484
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20759 0 0 0 53934 73 0 0 25 0 1 0 546837261 95109120 20011 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23220 20011 603 41 0 23179 0
vsize: 92880
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 20933 0 0 0 54933 73 0 0 25 0 1 0 546837261 95805440 20185 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23390 20185 603 41 0 23349 0
vsize: 93560
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 21124 0 0 0 55932 74 0 0 25 0 1 0 546837261 96604160 20376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23585 20376 603 41 0 23544 0
vsize: 94340
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 21276 0 0 0 56932 75 0 0 25 0 1 0 546837261 97161216 20528 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23721 20528 603 41 0 23680 0
vsize: 94884
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 21430 0 0 0 57930 77 0 0 25 0 1 0 546837261 97828864 20682 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23884 20682 603 41 0 23843 0
vsize: 95536
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 21584 0 0 0 58930 77 0 0 25 0 1 0 546837261 98521088 20836 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24053 20836 603 41 0 24012 0
vsize: 96212
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 21730 0 0 0 59929 78 0 0 25 0 1 0 546837261 99057664 20982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24184 20982 603 41 0 24143 0
vsize: 96736
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 21910 0 0 0 60929 79 0 0 25 0 1 0 546837261 99860480 21162 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24380 21162 603 41 0 24339 0
vsize: 97520
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22008 0 0 0 61928 79 0 0 25 0 1 0 546837261 100261888 21260 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24478 21260 603 41 0 24437 0
vsize: 97912
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22119 0 0 0 62928 80 0 0 25 0 1 0 546837261 100667392 21371 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24577 21371 603 41 0 24536 0
vsize: 98308
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22253 0 0 0 63927 81 0 0 25 0 1 0 546837261 101335040 21505 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24740 21505 603 41 0 24699 0
vsize: 98960
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22359 0 0 0 64926 82 0 0 25 0 1 0 546837261 101752832 21611 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24842 21611 603 41 0 24801 0
vsize: 99368
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22447 0 0 0 65926 83 0 0 25 0 1 0 546837261 102023168 21699 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24908 21699 603 41 0 24867 0
vsize: 99632
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22522 0 0 0 66925 83 0 0 25 0 1 0 546837261 102293504 21774 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24974 21774 603 41 0 24933 0
vsize: 99896
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22588 0 0 0 67925 84 0 0 25 0 1 0 546837261 102559744 21840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25039 21840 603 41 0 24998 0
vsize: 100156
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22647 0 0 0 68925 84 0 0 25 0 1 0 546837261 102825984 21899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25104 21899 603 41 0 25063 0
vsize: 100416
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22706 0 0 0 69924 85 0 0 25 0 1 0 546837261 102961152 21958 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25137 21958 603 41 0 25096 0
vsize: 100548
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22769 0 0 0 70924 85 0 0 25 0 1 0 546837261 103231488 22021 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25203 22021 603 41 0 25162 0
vsize: 100812
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22851 0 0 0 71924 86 0 0 25 0 1 0 546837261 103497728 22103 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25268 22103 603 41 0 25227 0
vsize: 101072
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 22932 0 0 0 72923 87 0 0 25 0 1 0 546837261 103956480 22184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25380 22184 603 41 0 25339 0
vsize: 101520
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23014 0 0 0 73922 88 0 0 25 0 1 0 546837261 104304640 22266 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25465 22266 603 41 0 25424 0
vsize: 101860
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23058 0 0 0 74922 88 0 0 25 0 1 0 546837261 104435712 22310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25497 22310 603 41 0 25456 0
vsize: 101988
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23128 0 0 0 75922 88 0 0 25 0 1 0 546837261 104697856 22380 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25561 22380 603 41 0 25520 0
vsize: 102244
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23178 0 0 0 76921 89 0 0 25 0 1 0 546837261 104964096 22430 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25626 22430 603 41 0 25585 0
vsize: 102504
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23243 0 0 0 77921 90 0 0 25 0 1 0 546837261 105246720 22495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25695 22495 603 41 0 25654 0
vsize: 102780
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23310 0 0 0 78920 90 0 0 25 0 1 0 546837261 105512960 22562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25760 22562 603 41 0 25719 0
vsize: 103040
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23378 0 0 0 79920 90 0 0 25 0 1 0 546837261 105779200 22630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25825 22630 603 41 0 25784 0
vsize: 103300
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23481 0 0 0 80920 91 0 0 25 0 1 0 546837261 106184704 22733 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25924 22733 603 41 0 25883 0
vsize: 103696
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23566 0 0 0 81920 91 0 0 25 0 1 0 546837261 106455040 22818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25990 22818 603 41 0 25949 0
vsize: 103960
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23696 0 0 0 82919 92 0 0 25 0 1 0 546837261 106987520 22948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26120 22948 603 41 0 26079 0
vsize: 104480
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23806 0 0 0 83919 92 0 0 25 0 1 0 546837261 107388928 23058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26218 23058 603 41 0 26177 0
vsize: 104872
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 23915 0 0 0 84918 93 0 0 25 0 1 0 546837261 107921408 23167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26348 23167 603 41 0 26307 0
vsize: 105392
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24033 0 0 0 85918 94 0 0 25 0 1 0 546837261 108466176 23285 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26481 23285 603 41 0 26440 0
vsize: 105924
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24149 0 0 0 86917 95 0 0 25 0 1 0 546837261 108863488 23401 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26578 23401 603 41 0 26537 0
vsize: 106312
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24255 0 0 0 87917 95 0 0 25 0 1 0 546837261 109408256 23507 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26711 23507 603 41 0 26670 0
vsize: 106844
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24350 0 0 0 88917 96 0 0 25 0 1 0 546837261 109711360 23602 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26785 23602 603 41 0 26744 0
vsize: 107140
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24413 0 0 0 89917 96 0 0 25 0 1 0 546837261 109977600 23665 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26850 23665 603 41 0 26809 0
vsize: 107400
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24481 0 0 0 90917 96 0 0 25 0 1 0 546837261 110292992 23733 4294967295 134512640 134672761 3221224544 3221223728 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26927 23733 603 41 0 26886 0
vsize: 107708
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24625 0 0 0 91917 96 0 0 25 0 1 0 546837261 110952448 23877 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27088 23877 603 41 0 27047 0
vsize: 108352
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24739 0 0 0 92917 96 0 0 25 0 1 0 546837261 111484928 23991 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27218 23991 603 41 0 27177 0
vsize: 108872
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24838 0 0 0 93917 97 0 0 25 0 1 0 546837261 111890432 24090 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27317 24090 603 41 0 27276 0
vsize: 109268
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 24952 0 0 0 94917 97 0 0 25 0 1 0 546837261 112291840 24204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27415 24204 603 41 0 27374 0
vsize: 109660
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25226 0 0 0 95916 98 0 0 25 0 1 0 546837261 113360896 24478 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27676 24478 603 41 0 27635 0
vsize: 110704
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25354 0 0 0 96915 99 0 0 25 0 1 0 546837261 114946048 24606 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28063 24606 603 41 0 28022 0
vsize: 112252
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25436 0 0 0 97915 99 0 0 25 0 1 0 546837261 115228672 24688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28132 24688 603 41 0 28091 0
vsize: 112528
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25533 0 0 0 98915 99 0 0 25 0 1 0 546837261 115679232 24785 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28242 24785 603 41 0 28201 0
vsize: 112968
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25604 0 0 0 99915 99 0 0 25 0 1 0 546837261 116129792 24856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28352 24856 603 41 0 28311 0
vsize: 113408
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25639 0 0 0 100915 99 0 0 25 0 1 0 546837261 116129792 24891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28352 24891 603 41 0 28311 0
vsize: 113408
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25691 0 0 0 101915 99 0 0 25 0 1 0 546837261 116400128 24943 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28418 24943 603 41 0 28377 0
vsize: 113672
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25732 0 0 0 102915 100 0 0 25 0 1 0 546837261 116535296 24984 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28451 24984 603 41 0 28410 0
vsize: 113804
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25800 0 0 0 103915 100 0 0 25 0 1 0 546837261 116805632 25052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28517 25052 603 41 0 28476 0
vsize: 114068
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 25915 0 0 0 104915 100 0 0 25 0 1 0 546837261 117342208 25167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28648 25167 603 41 0 28607 0
vsize: 114592
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 26074 0 0 0 105915 101 0 0 25 0 1 0 546837261 117891072 25326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28782 25326 603 41 0 28741 0
vsize: 115128
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 26267 0 0 0 106915 101 0 0 25 0 1 0 546837261 118685696 25519 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28976 25519 603 41 0 28935 0
vsize: 115904
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 26448 0 0 0 107915 101 0 0 25 0 1 0 546837261 119504896 25700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29176 25700 603 41 0 29135 0
vsize: 116704
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 26608 0 0 0 108915 101 0 0 25 0 1 0 546837261 120176640 25860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29340 25860 603 41 0 29299 0
vsize: 117360
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 26753 0 0 0 109915 102 0 0 25 0 1 0 546837261 120729600 26005 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29475 26005 603 41 0 29434 0
vsize: 117900
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 26892 0 0 0 110914 102 0 0 25 0 1 0 546837261 121266176 26144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29606 26144 603 41 0 29565 0
vsize: 118424
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27013 0 0 0 111914 102 0 0 25 0 1 0 546837261 121921536 26265 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29766 26265 603 41 0 29725 0
vsize: 119064
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27042 0 0 0 112913 103 0 0 25 0 1 0 546837261 121921536 26294 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29766 26294 603 41 0 29725 0
vsize: 119064
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27113 0 0 0 113913 103 0 0 25 0 1 0 546837261 122404864 26365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29884 26365 603 41 0 29843 0
vsize: 119536
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27172 0 0 0 114913 103 0 0 25 0 1 0 546837261 122540032 26424 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29917 26424 603 41 0 29876 0
vsize: 119668
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27224 0 0 0 115913 103 0 0 25 0 1 0 546837261 122814464 26476 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29984 26476 603 41 0 29943 0
vsize: 119936
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27278 0 0 0 116913 103 0 0 25 0 1 0 546837261 123088896 26530 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30051 26530 603 41 0 30010 0
vsize: 120204
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27333 0 0 0 117913 104 0 0 25 0 1 0 546837261 123219968 26585 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 26585 603 41 0 30042 0
vsize: 120332
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27387 0 0 0 118913 104 0 0 25 0 1 0 546837261 123490304 26639 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30149 26639 603 41 0 30108 0
vsize: 120596
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 9761
Raw data (stat): 9761 (minisat+) R 9760 28099 28098 0 -1 0 27433 0 0 0 119913 104 0 0 25 0 1 0 546837261 123621376 26685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30181 26685 603 41 0 30140 0
vsize: 120724
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.97 1/54 9761
Raw data (stat): 9761 (minisat+) Z 9760 28099 28098 0 -1 12 27435 0 0 0 119913 109 0 0 25 0 1 0 546837261 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.23
CPU user time (s): 1199.13
CPU system time (s): 1.09983
CPU usage (%): 100.014
Max. virtual memory (Kb): 120724
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####