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-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-bg512142.opb
MD5SUM	bad364b24a8c9bb1cd282751f54245c6
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	9600
Biggest coefficient in the objective function	5368709120000
Number of bits for the biggest coefficient in the objective function	43
Sum of the numbers in the objective function	773893279252632
Number of bits of the sum of numbers in the objective function	50
Biggest number in a constraint	5368709120000
Number of bits of the biggest number in a constraint	43
Biggest sum of numbers in a constraint	773893279252632
Number of bits of the biggest sum of numbers	50
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1210.55
Number of variables	16800
Total number of constraints	1307
Number of constraints which are clauses	11
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1296
Minimum length of a constraint	1
Maximum length of a constraint	183
Trace number 30936

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-05-25 20:58:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22333 boxname=wulflinc28 idbench=1149 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  bad364b24a8c9bb1cd282751f54245c6  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-bg512142.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-bg512142.opb
IDLAUNCH: 22333
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        811248 kB
Buffers:         30860 kB
Cached:         170472 kB
SwapCached:        832 kB
Active:          18916 kB
Inactive:       184724 kB
HighTotal:      131008 kB
HighFree:        84980 kB
LowTotal:       903652 kB
LowFree:        726268 kB
SwapTotal:     2097640 kB
SwapFree:      2096192 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5444 kB
Slab:            13984 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 21:18:46 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 22333 7 1229.9 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1171 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1283]---> Sorter-cost: 1324     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1282]---> Sorter-cost:  785     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1281]---> Sorter-cost: 1347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1280]---> Sorter-cost: 1303     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1279]---> Sorter-cost:  761     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1278]---> Sorter-cost: 1307     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1277]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1270]---> Sorter-cost: 1338     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1269]---> Sorter-cost: 1146     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1268]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1267]---> Sorter-cost:  795     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1266]---> Sorter-cost: 1307     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1265]---> BDD-cost:  147
c ---[1264]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1259]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1258]---> Sorter-cost: 1297     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1257]---> Sorter-cost: 1466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1256]---> Sorter-cost: 1595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1247]---> Sorter-cost: 1427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1241]---> Sorter-cost: 1320     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1240]---> Sorter-cost: 1276     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1239]---> Sorter-cost: 1307     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1237]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1236]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1235]---> Sorter-cost:  766     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1234]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1232]---> Sorter-cost: 1483     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1231]---> Sorter-cost:  783     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1230]---> Sorter-cost: 1365     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1227]---> Sorter-cost: 1183     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1226]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1225]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1224]---> Sorter-cost: 1328     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> Sorter-cost:  870     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1222]---> Sorter-cost:  839     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1218]---> Sorter-cost:  901     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1212]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1211]---> Sorter-cost: 1449     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1206]---> Sorter-cost: 1200     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1205]---> Sorter-cost: 1409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1204]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1202]---> Sorter-cost: 1392     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1201]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1199]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1198]---> BDD-cost:  129
c ---[1195]---> Sorter-cost:  913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1194]---> Sorter-cost:  766     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1193]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1190]---> Sorter-cost:  813     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1188]---> Sorter-cost:  798     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1186]---> Sorter-cost:  837     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1184]---> BDD-cost:  190
c ---[1182]---> Sorter-cost:  852     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1180]---> Sorter-cost:  852     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1178]---> Sorter-cost: 1338     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1176]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1174]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1172]---> Sorter-cost: 1383     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1170]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1168]---> Sorter-cost: 1413     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1166]---> Sorter-cost: 1419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost: 1434     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1162]---> Sorter-cost: 1427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1160]---> Sorter-cost: 1427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1158]---> Sorter-cost: 1427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1156]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1154]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1152]---> Sorter-cost: 1395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1150]---> Sorter-cost: 1376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1148]---> Sorter-cost: 1376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Sorter-cost: 1353     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1144]---> Sorter-cost: 1325     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1142]---> Sorter-cost: 1325     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1140]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1138]---> Sorter-cost: 1274     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1136]---> Sorter-cost: 1242     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1134]---> Sorter-cost: 1149     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1132]---> Sorter-cost: 1297     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1130]---> Sorter-cost: 1345     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1128]---> Sorter-cost: 1378     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1126]---> Sorter-cost: 1359     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1124]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1122]---> Sorter-cost: 1389     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1120]---> Sorter-cost: 1381     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1118]---> Sorter-cost: 1396     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1116]---> Sorter-cost: 1392     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1114]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1112]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1110]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1108]---> Sorter-cost: 1395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1106]---> Sorter-cost: 1372     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> Sorter-cost: 1353     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1102]---> Sorter-cost: 1353     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1100]---> Sorter-cost: 1344     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1098]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1096]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1094]---> Sorter-cost: 1293     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1092]---> Sorter-cost: 1251     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1090]---> Sorter-cost: 1242     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1088]---> Sorter-cost: 1149     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1086]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1084]---> Sorter-cost: 1411     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1082]---> Sorter-cost: 1444     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1080]---> Sorter-cost: 1425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1078]---> Sorter-cost: 1440     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1076]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1074]---> Sorter-cost: 1428     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1072]---> Sorter-cost: 1443     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1070]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1068]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1066]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1064]---> Sorter-cost: 1446     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1062]---> Sorter-cost: 1446     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1060]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1058]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1056]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1054]---> Sorter-cost: 1395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1052]---> Sorter-cost: 1353     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1050]---> Sorter-cost: 1353     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1048]---> Sorter-cost: 1344     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1046]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1044]---> Sorter-cost: 1270     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1042]---> Sorter-cost: 1200     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1040]---> Sorter-cost:  862     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1038]---> Sorter-cost:  878     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1036]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1034]---> Sorter-cost:  909     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1032]---> Sorter-cost:  924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1030]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1028]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1026]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1024]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1022]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1020]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1018]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1016]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1014]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1012]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1010]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1008]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1006]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1004]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1002]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1000]---> Sorter-cost:  881     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 998]---> Sorter-cost:  856     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 996]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 994]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 992]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 990]---> Sorter-cost: 1434     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 988]---> Sorter-cost: 1440     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 986]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 984]---> Sorter-cost: 1470     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 982]---> Sorter-cost: 1462     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 980]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 978]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 976]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 974]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 972]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 970]---> Sorter-cost: 1446     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 968]---> Sorter-cost: 1423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 966]---> Sorter-cost: 1423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 964]---> Sorter-cost: 1423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 962]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 960]---> Sorter-cost: 1372     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 958]---> Sorter-cost: 1372     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 956]---> Sorter-cost: 1344     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Sorter-cost: 1270     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 950]---> Sorter-cost: 1219     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 948]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 946]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 944]---> Sorter-cost: 1434     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 942]---> Sorter-cost: 1449     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 940]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 938]---> Sorter-cost: 1479     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 936]---> Sorter-cost: 1494     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 934]---> Sorter-cost: 1506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 932]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 930]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 928]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 926]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 924]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 922]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 920]---> Sorter-cost: 1446     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 918]---> Sorter-cost: 1446     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 916]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 914]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 912]---> Sorter-cost: 1395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 910]---> Sorter-cost: 1353     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 908]---> Sorter-cost: 1344     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 906]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 904]---> Sorter-cost: 1251     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 902]---> BDD-cost:   80
c ---[ 900]---> BDD-cost:   71
c ---[ 898]---> BDD-cost:   80
c ---[ 896]---> BDD-cost:   85
c ---[ 894]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 892]---> Sorter-cost:  505     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 890]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 888]---> Sorter-cost:  535     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 886]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 884]---> Sorter-cost:  565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 882]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 880]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 878]---> Sorter-cost:  610     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 876]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 874]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 872]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 870]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 868]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 866]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 864]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 862]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 860]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 858]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 856]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 854]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 852]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 850]---> Sorter-cost:  568     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 848]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 846]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 844]---> Sorter-cost:  496     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 842]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 840]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 838]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 836]---> Sorter-cost:  556     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 834]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 832]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 830]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 828]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 826]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 824]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 822]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 820]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 818]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 816]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 814]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 810]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 808]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 806]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 804]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 802]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 800]---> Sorter-cost:  505     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 798]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 796]---> Sorter-cost:  535     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 794]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 792]---> Sorter-cost:  565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 790]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 788]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost:  601     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 776]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 770]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  568     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  515     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  529     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost:  574     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost:  589     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Sorter-cost:  610     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 740]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 738]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 736]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 732]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 730]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 728]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 726]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 724]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 720]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 718]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 716]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 711]---> BDD-cost:   89
c ---[ 710]---> BDD-cost:  113
c ---[ 709]---> BDD-cost:  113
c ---[ 708]---> BDD-cost:  113
c ---[ 707]---> BDD-cost:  113
c ---[ 706]---> BDD-cost:  113
c ---[ 705]---> BDD-cost:  113
c ---[ 704]---> BDD-cost:  113
c ---[ 703]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:  113
c ---[ 701]---> BDD-cost:  113
c ---[ 700]---> BDD-cost:  113
c ---[ 699]---> BDD-cost:  109
c ---[ 698]---> BDD-cost:  109
c ---[ 697]---> BDD-cost:  109
c ---[ 696]---> BDD-cost:  109
c ---[ 695]---> BDD-cost:  109
c ---[ 694]---> BDD-cost:  105
c ---[ 693]---> BDD-cost:  105
c ---[ 692]---> BDD-cost:  105
c ---[ 691]---> BDD-cost:   85
c ---[ 690]---> BDD-cost:  109
c ---[ 689]---> BDD-cost:  109
c ---[ 688]---> BDD-cost:  109
c ---[ 687]---> BDD-cost:  109
c ---[ 686]---> BDD-cost:  109
c ---[ 685]---> BDD-cost:  109
c ---[ 684]---> BDD-cost:  109
c ---[ 683]---> BDD-cost:  109
c ---[ 682]---> BDD-cost:  105
c ---[ 681]---> BDD-cost:  105
c ---[ 680]---> BDD-cost:  105
c ---[ 679]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:  105
c ---[ 677]---> BDD-cost:  105
c ---[ 676]---> BDD-cost:   94
c ---[ 675]---> BDD-cost:   89
c ---[ 674]---> BDD-cost:  116
c ---[ 673]---> BDD-cost:  116
c ---[ 672]---> BDD-cost:  116
c ---[ 671]---> BDD-cost:  116
c ---[ 670]---> BDD-cost:  116
c ---[ 669]---> BDD-cost:  116
c ---[ 668]---> BDD-cost:  112
c ---[ 667]---> BDD-cost:  112
c ---[ 666]---> BDD-cost:  112
c ---[ 665]---> BDD-cost:  112
c ---[ 664]---> BDD-cost:  112
c ---[ 663]---> BDD-cost:  112
c ---[ 662]---> BDD-cost:  112
c ---[ 661]---> BDD-cost:  104
c ---[ 660]---> BDD-cost:  104
c ---[ 659]---> BDD-cost:  104
c ---[ 658]---> BDD-cost:   93
c ---[ 657]---> BDD-cost:  120
c ---[ 656]---> BDD-cost:  120
c ---[ 655]---> BDD-cost:  120
c ---[ 654]---> BDD-cost:  119
c ---[ 653]---> BDD-cost:  120
c ---[ 652]---> BDD-cost:  120
c ---[ 651]---> BDD-cost:  116
c ---[ 650]---> BDD-cost:  116
c ---[ 649]---> BDD-cost:  115
c ---[ 648]---> BDD-cost:  115
c ---[ 647]---> BDD-cost:  116
c ---[ 646]---> BDD-cost:  116
c ---[ 645]---> BDD-cost:  116
c ---[ 644]---> BDD-cost:  112
c ---[ 643]---> BDD-cost:  112
c ---[ 642]---> BDD-cost:  112
c ---[ 641]---> BDD-cost:  112
c ---[ 640]---> BDD-cost:  104
c ---[ 639]---> BDD-cost:  104
c ---[ 638]---> BDD-cost:   93
c ---[ 637]---> BDD-cost:  123
c ---[ 636]---> BDD-cost:  123
c ---[ 635]---> BDD-cost:  123
c ---[ 634]---> BDD-cost:  123
c ---[ 633]---> BDD-cost:  123
c ---[ 632]---> BDD-cost:  123
c ---[ 631]---> BDD-cost:  119
c ---[ 630]---> BDD-cost:  119
c ---[ 629]---> BDD-cost:  119
c ---[ 628]---> BDD-cost:  119
c ---[ 627]---> BDD-cost:  119
c ---[ 626]---> BDD-cost:  119
c ---[ 625]---> BDD-cost:  119
c ---[ 624]---> BDD-cost:  111
c ---[ 623]---> BDD-cost:  111
c ---[ 622]---> BDD-cost:  111
c ---[ 621]---> BDD-cost:   89
c ---[ 620]---> BDD-cost:  113
c ---[ 619]---> BDD-cost:  113
c ---[ 618]---> BDD-cost:  113
c ---[ 617]---> BDD-cost:  113
c ---[ 616]---> BDD-cost:  113
c ---[ 615]---> BDD-cost:  113
c ---[ 614]---> BDD-cost:  113
c ---[ 613]---> BDD-cost:  113
c ---[ 612]---> BDD-cost:  113
c ---[ 611]---> BDD-cost:  113
c ---[ 610]---> BDD-cost:  113
c ---[ 609]---> BDD-cost:  113
c ---[ 608]---> BDD-cost:  109
c ---[ 607]---> BDD-cost:  109
c ---[ 606]---> BDD-cost:  109
c ---[ 605]---> BDD-cost:  108
c ---[ 604]---> BDD-cost:  104
c ---[ 603]---> BDD-cost:  104
c ---[ 602]---> BDD-cost:  105
c ---[ 601]---> BDD-cost:   94
c ---[ 600]---> BDD-cost:   93
c ---[ 599]---> BDD-cost:  120
c ---[ 598]---> BDD-cost:  120
c ---[ 597]---> BDD-cost:  120
c ---[ 596]---> BDD-cost:  120
c ---[ 595]---> BDD-cost:  120
c ---[ 594]---> BDD-cost:  120
c ---[ 593]---> BDD-cost:  120
c ---[ 592]---> BDD-cost:  120
c ---[ 591]---> BDD-cost:  120
c ---[ 590]---> BDD-cost:  120
c ---[ 589]---> BDD-cost:  120
c ---[ 588]---> BDD-cost:  116
c ---[ 587]---> BDD-cost:  116
c ---[ 586]---> BDD-cost:  116
c ---[ 585]---> BDD-cost:  116
c ---[ 584]---> BDD-cost:  115
c ---[ 583]---> BDD-cost:  111
c ---[ 582]---> BDD-cost:  111
c ---[ 581]---> BDD-cost:  112
c ---[ 580]---> BDD-cost:  104
c ---[ 579]---> BDD-cost:   89
c ---[ 578]---> BDD-cost:  112
c ---[ 577]---> BDD-cost:  113
c ---[ 576]---> BDD-cost:  113
c ---[ 575]---> BDD-cost:  113
c ---[ 574]---> BDD-cost:  113
c ---[ 573]---> BDD-cost:  113
c ---[ 572]---> BDD-cost:  109
c ---[ 571]---> BDD-cost:  109
c ---[ 570]---> BDD-cost:  109
c ---[ 569]---> BDD-cost:  108
c ---[ 568]---> BDD-cost:  108
c ---[ 567]---> BDD-cost:  109
c ---[ 566]---> BDD-cost:  109
c ---[ 565]---> BDD-cost:  101
c ---[ 564]---> BDD-cost:  101
c ---[ 563]---> BDD-cost:  101
c ---[ 562]---> BDD-cost:   93
c ---[ 561]---> BDD-cost:   70
c ---[ 560]---> BDD-cost:  117
c ---[ 559]---> BDD-cost:  117
c ---[ 558]---> BDD-cost:  113
c ---[ 557]---> BDD-cost:  113
c ---[ 556]---> BDD-cost:  113
c ---[ 555]---> BDD-cost:  113
c ---[ 554]---> BDD-cost:  113
c ---[ 553]---> BDD-cost:  113
c ---[ 552]---> BDD-cost:  113
c ---[ 551]---> BDD-cost:  113
c ---[ 550]---> BDD-cost:  112
c ---[ 549]---> BDD-cost:  108
c ---[ 548]---> BDD-cost:  109
c ---[ 547]---> BDD-cost:  109
c ---[ 546]---> BDD-cost:  109
c ---[ 545]---> BDD-cost:  109
c ---[ 544]---> BDD-cost:  101
c ---[ 543]---> BDD-cost:  101
c ---[ 542]---> BDD-cost:   93
c ---[ 541]---> BDD-cost:  117
c ---[ 540]---> BDD-cost:  117
c ---[ 539]---> BDD-cost:  117
c ---[ 538]---> BDD-cost:  117
c ---[ 537]---> BDD-cost:  117
c ---[ 536]---> BDD-cost:  117
c ---[ 535]---> BDD-cost:  117
c ---[ 534]---> BDD-cost:  117
c ---[ 533]---> BDD-cost:  113
c ---[ 532]---> BDD-cost:  113
c ---[ 531]---> BDD-cost:  113
c ---[ 530]---> BDD-cost:  113
c ---[ 529]---> BDD-cost:  113
c ---[ 528]---> BDD-cost:  113
c ---[ 527]---> BDD-cost:  109
c ---[ 526]---> BDD-cost:  109
c ---[ 525]---> BDD-cost:  109
c ---[ 524]---> BDD-cost:  109
c ---[ 523]---> BDD-cost:   54
c ---[ 522]---> BDD-cost:   20
c ---[ 521]---> BDD-cost:   32
c ---[ 520]---> BDD-cost:   30
c ---[ 519]---> BDD-cost:   31
c ---[ 518]---> BDD-cost:   31
c ---[ 517]---> BDD-cost:   31
c ---[ 516]---> BDD-cost:   32
c ---[ 515]---> BDD-cost:   32
c ---[ 514]---> BDD-cost:   32
c ---[ 513]---> BDD-cost:   30
c ---[ 512]---> BDD-cost:   32
c ---[ 511]---> BDD-cost:   32
c ---[ 510]---> BDD-cost:   28
c ---[ 509]---> BDD-cost:   30
c ---[ 508]---> BDD-cost:   25
c ---[ 507]---> BDD-cost:   30
c ---[ 506]---> BDD-cost:   30
c ---[ 505]---> BDD-cost:   24
c ---[ 504]---> BDD-cost:   28
c ---[ 503]---> BDD-cost:   28
c ---[ 502]---> BDD-cost:   25
c ---[ 501]---> BDD-cost:   24
c ---[ 500]---> BDD-cost:   23
c ---[ 499]---> BDD-cost:   20
c ---[ 498]---> BDD-cost:   19
c ---[ 497]---> BDD-cost:   24
c ---[ 496]---> BDD-cost:   29
c ---[ 495]---> BDD-cost:   29
c ---[ 494]---> BDD-cost:   27
c ---[ 493]---> BDD-cost:   30
c ---[ 492]---> BDD-cost:   27
c ---[ 491]---> BDD-cost:   27
c ---[ 490]---> BDD-cost:   29
c ---[ 489]---> BDD-cost:   27
c ---[ 488]---> BDD-cost:   24
c ---[ 487]---> BDD-cost:   28
c ---[ 486]---> BDD-cost:   26
c ---[ 485]---> BDD-cost:   28
c ---[ 484]---> BDD-cost:   26
c ---[ 483]---> BDD-cost:   23
c ---[ 482]---> BDD-cost:   26
c ---[ 481]---> BDD-cost:   25
c ---[ 480]---> BDD-cost:   24
c ---[ 479]---> BDD-cost:   24
c ---[ 478]---> BDD-cost:   24
c ---[ 477]---> BDD-cost:   22
c ---[ 476]---> BDD-cost:   22
c ---[ 475]---> BDD-cost:   18
c ---[ 474]---> BDD-cost:   20
c ---[ 473]---> BDD-cost:   30
c ---[ 472]---> BDD-cost:   32
c ---[ 471]---> BDD-cost:   32
c ---[ 470]---> BDD-cost:   32
c ---[ 469]---> BDD-cost:   30
c ---[ 468]---> BDD-cost:   31
c ---[ 467]---> BDD-cost:   30
c ---[ 466]---> BDD-cost:   30
c ---[ 465]---> BDD-cost:   29
c ---[ 464]---> BDD-cost:   30
c ---[ 463]---> BDD-cost:   30
c ---[ 462]---> BDD-cost:   30
c ---[ 461]---> BDD-cost:   30
c ---[ 460]---> BDD-cost:   28
c ---[ 459]---> BDD-cost:   28
c ---[ 458]---> BDD-cost:   25
c ---[ 457]---> BDD-cost:   28
c ---[ 456]---> BDD-cost:   25
c ---[ 455]---> BDD-cost:   22
c ---[ 454]---> BDD-cost:   26
c ---[ 453]---> BDD-cost:   23
c ---[ 452]---> BDD-cost:   23
c ---[ 451]---> BDD-cost:   20
c ---[ 450]---> BDD-cost:   21
c ---[ 449]---> BDD-cost:   33
c ---[ 448]---> BDD-cost:   34
c ---[ 447]---> BDD-cost:   30
c ---[ 446]---> BDD-cost:   34
c ---[ 445]---> BDD-cost:   33
c ---[ 444]---> BDD-cost:   34
c ---[ 443]---> BDD-cost:   30
c ---[ 442]---> BDD-cost:   32
c ---[ 441]---> BDD-cost:   32
c ---[ 440]---> BDD-cost:   32
c ---[ 439]---> BDD-cost:   31
c ---[ 438]---> BDD-cost:   30
c ---[ 437]---> BDD-cost:   31
c ---[ 436]---> BDD-cost:   30
c ---[ 435]---> BDD-cost:   29
c ---[ 434]---> BDD-cost:   29
c ---[ 433]---> BDD-cost:   28
c ---[ 432]---> BDD-cost:   28
c ---[ 431]---> BDD-cost:   27
c ---[ 430]---> BDD-cost:   28
c ---[ 429]---> BDD-cost:   24
c ---[ 428]---> BDD-cost:   23
c ---[ 427]---> BDD-cost:   21
c ---[ 426]---> BDD-cost:   21
c ---[ 425]---> BDD-cost:   34
c ---[ 424]---> BDD-cost:   33
c ---[ 423]---> BDD-cost:   32
c ---[ 422]---> BDD-cost:   33
c ---[ 421]---> BDD-cost:   34
c ---[ 420]---> BDD-cost:   34
c ---[ 419]---> BDD-cost:   32
c ---[ 418]---> BDD-cost:   32
c ---[ 417]---> BDD-cost:   31
c ---[ 416]---> BDD-cost:   32
c ---[ 415]---> BDD-cost:   31
c ---[ 414]---> BDD-cost:   29
c ---[ 413]---> BDD-cost:   31
c ---[ 412]---> BDD-cost:   28
c ---[ 411]---> BDD-cost:   30
c ---[ 410]---> BDD-cost:   28
c ---[ 409]---> BDD-cost:   29
c ---[ 408]---> BDD-cost:   27
c ---[ 407]---> BDD-cost:   27
c ---[ 406]---> BDD-cost:   28
c ---[ 405]---> BDD-cost:   26
c ---[ 404]---> BDD-cost:   24
c ---[ 403]---> BDD-cost:   21
c ---[ 401]---> BDD-cost:   30
c ---[ 400]---> BDD-cost:   32
c ---[ 399]---> BDD-cost:   32
c ---[ 398]---> BDD-cost:   32
c ---[ 397]---> BDD-cost:   32
c ---[ 396]---> BDD-cost:   31
c ---[ 395]---> BDD-cost:   32
c ---[ 394]---> BDD-cost:   32
c ---[ 393]---> BDD-cost:   27
c ---[ 392]---> BDD-cost:   32
c ---[ 391]---> BDD-cost:   29
c ---[ 390]---> BDD-cost:   32
c ---[ 389]---> BDD-cost:   29
c ---[ 388]---> BDD-cost:   30
c ---[ 387]---> BDD-cost:   30
c ---[ 386]---> BDD-cost:   30
c ---[ 385]---> BDD-cost:   28
c ---[ 384]---> BDD-cost:   28
c ---[ 383]---> BDD-cost:   28
c ---[ 382]---> BDD-cost:   24
c ---[ 381]---> BDD-cost:   26
c ---[ 380]---> BDD-cost:   24
c ---[ 379]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:   33
c ---[ 376]---> BDD-cost:   30
c ---[ 375]---> BDD-cost:   34
c ---[ 374]---> BDD-cost:   33
c ---[ 373]---> BDD-cost:   33
c ---[ 372]---> BDD-cost:   34
c ---[ 371]---> BDD-cost:   34
c ---[ 370]---> BDD-cost:   33
c ---[ 369]---> BDD-cost:   34
c ---[ 368]---> BDD-cost:   33
c ---[ 367]---> BDD-cost:   34
c ---[ 366]---> BDD-cost:   32
c ---[ 365]---> BDD-cost:   32
c ---[ 364]---> BDD-cost:   30
c ---[ 363]---> BDD-cost:   32
c ---[ 362]---> BDD-cost:   31
c ---[ 361]---> BDD-cost:   30
c ---[ 360]---> BDD-cost:   30
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   27
c ---[ 357]---> BDD-cost:   27
c ---[ 356]---> BDD-cost:   23
c ---[ 355]---> BDD-cost:   24
c ---[ 354]---> BDD-cost:   21
c ---[ 353]---> BDD-cost:   34
c ---[ 352]---> BDD-cost:   33
c ---[ 351]---> BDD-cost:   32
c ---[ 350]---> BDD-cost:   33
c ---[ 349]---> BDD-cost:   34
c ---[ 348]---> BDD-cost:   34
c ---[ 347]---> BDD-cost:   32
c ---[ 346]---> BDD-cost:   32
c ---[ 345]---> BDD-cost:   31
c ---[ 344]---> BDD-cost:   32
c ---[ 343]---> BDD-cost:   31
c ---[ 342]---> BDD-cost:   29
c ---[ 341]---> BDD-cost:   31
c ---[ 340]---> BDD-cost:   28
c ---[ 339]---> BDD-cost:   30
c ---[ 338]---> BDD-cost:   28
c ---[ 337]---> BDD-cost:   29
c ---[ 336]---> BDD-cost:   27
c ---[ 335]---> BDD-cost:   27
c ---[ 334]---> BDD-cost:   28
c ---[ 333]---> BDD-cost:   26
c ---[ 332]---> BDD-cost:   24
c ---[ 331]---> BDD-cost:   21
c ---[ 330]---> BDD-cost:   22
c ---[ 329]---> BDD-cost:   36
c ---[ 328]---> BDD-cost:   36
c ---[ 327]---> BDD-cost:   36
c ---[ 326]---> BDD-cost:   34
c ---[ 325]---> BDD-cost:   30
c ---[ 324]---> BDD-cost:   34
c ---[ 323]---> BDD-cost:   32
c ---[ 322]---> BDD-cost:   33
c ---[ 321]---> BDD-cost:   33
c ---[ 320]---> BDD-cost:   32
c ---[ 319]---> BDD-cost:   33
c ---[ 318]---> BDD-cost:   34
c ---[ 317]---> BDD-cost:   30
c ---[ 316]---> BDD-cost:   32
c ---[ 315]---> BDD-cost:   29
c ---[ 314]---> BDD-cost:   32
c ---[ 313]---> BDD-cost:   32
c ---[ 312]---> BDD-cost:   30
c ---[ 311]---> BDD-cost:   30
c ---[ 310]---> BDD-cost:   28
c ---[ 309]---> BDD-cost:   26
c ---[ 308]---> BDD-cost:   25
c ---[ 307]---> BDD-cost:   21
c ---[ 306]---> BDD-cost:   22
c ---[ 305]---> BDD-cost:   35
c ---[ 304]---> BDD-cost:   36
c ---[ 303]---> BDD-cost:   34
c ---[ 302]---> BDD-cost:   36
c ---[ 301]---> BDD-cost:   36
c ---[ 300]---> BDD-cost:   36
c ---[ 299]---> BDD-cost:   35
c ---[ 298]---> BDD-cost:   36
c ---[ 297]---> BDD-cost:   34
c ---[ 296]---> BDD-cost:   34
c ---[ 295]---> BDD-cost:   34
c ---[ 294]---> BDD-cost:   33
c ---[ 293]---> BDD-cost:   34
c ---[ 292]---> BDD-cost:   34
c ---[ 291]---> BDD-cost:   29
c ---[ 290]---> BDD-cost:   32
c ---[ 289]---> BDD-cost:   29
c ---[ 288]---> BDD-cost:   29
c ---[ 287]---> BDD-cost:   30
c ---[ 286]---> BDD-cost:   29
c ---[ 285]---> BDD-cost:   28
c ---[ 284]---> BDD-cost:   28
c ---[ 283]---> BDD-cost:   26
c ---[ 213]---> BDD-cost:   11
c ---[ 212]---> BDD-cost:    5
c ---[ 211]---> BDD-cost:   10
c ---[ 210]---> BDD-cost:    4
c ---[ 209]---> BDD-cost:   16
c ---[ 208]---> BDD-cost:    6
c ---[ 207]---> Sorter-cost:  496     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 206]---> Sorter-cost:  500     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  527     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 204]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 202]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  756     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  949     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost: 1805     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost: 1685     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1794     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost: 1835     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1774     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 194]---> BDD-cost:    6
c ---[ 193]---> BDD-cost:    7
c ---[ 192]---> BDD-cost:    4
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:    7
c ---[ 189]---> BDD-cost:    5
c ---[ 188]---> BDD-cost:    7
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:   23
c ---[ 185]---> BDD-cost:    6
c ---[ 184]---> BDD-cost:    6
c ---[ 183]---> BDD-cost:    6
c ---[ 182]---> BDD-cost:    7
c ---[ 181]---> BDD-cost:    5
c ---[ 180]---> BDD-cost:    7
c ---[ 179]---> BDD-cost:    7
c ---[ 178]---> BDD-cost:   15
c ---[ 177]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  609     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  552     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> BDD-cost:  145
c ---[ 173]---> BDD-cost:  146
c ---[ 172]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> BDD-cost:  151
c ---[ 170]---> BDD-cost:  161
c ---[ 169]---> Sorter-cost:  883     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  789     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1726     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1811     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1770     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 1749     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> BDD-cost:    6
c ---[ 159]---> BDD-cost:    7
c ---[ 158]---> BDD-cost:    6
c ---[ 157]---> BDD-cost:    6
c ---[ 156]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    9
c ---[ 153]---> BDD-cost:    6
c ---[ 152]---> BDD-cost:   13
c ---[ 151]---> BDD-cost:  154
c ---[ 150]---> BDD-cost:  161
c ---[ 149]---> BDD-cost:  142
c ---[ 148]---> Sorter-cost:  489     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost: 1121     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost: 1835     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:   19
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost:  556     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost:  493     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> Sorter-cost: 1279     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost:  164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost: 1873     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1832     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    8
c ---[ 127]---> BDD-cost:   22
c ---[ 126]---> BDD-cost:    8
c ---[ 125]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:   39
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost:  533     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:    8
c ---[ 118]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:   23
c ---[ 111]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> BDD-cost:  154
c ---[ 109]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   11
c ---[ 105]---> Sorter-cost:  942     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> BDD-cost:   19
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:    7
c ---[ 101]---> BDD-cost:   48
c ---[ 100]---> BDD-cost:   20
c ---[  99]---> BDD-cost:    4
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:  150
c ---[  96]---> BDD-cost:    8
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   55
c ---[  93]---> BDD-cost:    6
c ---[  92]---> Sorter-cost: 1189     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> BDD-cost:    8
c ---[  89]---> BDD-cost:   22
c ---[  88]---> BDD-cost:   15
c ---[  87]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> BDD-cost:   25
c ---[  85]---> BDD-cost:   39
c ---[  84]---> BDD-cost:   48
c ---[  83]---> BDD-cost:   35
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:    8
c ---[  80]---> BDD-cost:  154
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:    1
c ---[  77]---> BDD-cost:  136
c ---[  76]---> BDD-cost:  166
c ---[  75]---> Sorter-cost:  489     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   46
c ---[  72]---> BDD-cost:   45
c ---[  71]---> BDD-cost:   27
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   19
c ---[  68]---> Sorter-cost: 1186     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost: 1334     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost: 1334     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost: 1334     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost: 1334     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost: 1332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost: 1334     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1334     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost: 1334     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost: 1299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost: 1299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost: 1299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost: 1291     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1269     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1231     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> Sorter-cost: 1136     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1175     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost: 1158     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1270     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost: 1517     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost: 1517     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost: 1517     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1517     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1517     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost: 1431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost: 1431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost: 1371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost: 1409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost: 1366     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost: 1346     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1329     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost: 1347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost: 1291     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost: 1245     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost: 2058     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost: 2103     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost: 2103     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost: 2061     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost: 2061     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost: 2061     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost: 1963     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost: 1963     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost: 2016     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost: 1803     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost: 1971     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost: 1929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost: 1876     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost: 1929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost: 1929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost: 1930     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost: 1841     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost: 1746     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost: 1673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost: 1611     Base: 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 | 1151869  2735477 |  383956       0        0     nan |  0.000 % |
c |       100 | 1151793  2735313 |  422351      78      244     3.1 |  4.186 % |
c |       250 | 1151614  2734915 |  464586     194      658     3.4 |  4.199 % |
c |       475 | 1151354  2734334 |  511045     382     1294     3.4 |  4.217 % |
c |       812 | 1150961  2733460 |  562149     652     2255     3.5 |  4.244 % |
c |      1318 | 1150255  2731882 |  618364    1065     3668     3.4 |  4.291 % |
c |      2077 | 1149517  2730235 |  680201    1705     5867     3.4 |  4.342 % |
c |      3216 | 1147929  2726680 |  748221    2600     9520     3.7 |  4.454 % |
c |      4924 | 1145433  2721100 |  823043    3939    14236     3.6 |  4.621 % |
c |      7486 | 1142489  2714493 |  905348    6079    22435     3.7 |  4.823 % |
c |     11330 | 1138896  2706523 |  995882    9411    37446     4.0 |  5.073 % |
c |     17096 | 1132896  2693013 | 1095471   14488    62545     4.3 |  5.491 % |
c |     25745 | 1126381  2678354 | 1205018   22354   121500     5.4 |  5.947 % |
c |     38719 | 1123246  2671285 | 1325520   34982   421212    12.0 |  6.165 % |
c |     58180 | 1117809  2658927 | 1458072   53897   740932    13.7 |  6.551 % |
c |     87377 | 1113265  2648690 | 1603879   82572  1341834    16.3 |  6.862 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  9144 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.84 0.94 0.90 2/54 9140
Raw data (stat): 9140 (runsolver) R 9139 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841946216 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0009 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0005 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0009 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0011 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.006 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0059 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 9144
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.007 s]
Raw data (loadavg): 0.97 0.95 0.91 3/58 9180
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9197
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9197
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9197
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9197
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9197
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9197
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9199
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.06 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.06 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.78 s]
Raw data (loadavg): 1.03 0.99 0.91 1/53 9201
Raw data (stat): 9140 (minisat+_script) S 9139 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841946216 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.78
CPU time (s): 1229.9
CPU user time (s): 1228.62
CPU system time (s): 1.28181
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####