PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-sctap2.opb
MD5SUM	c56066a13a725fcc9c143db3d9f8cc06
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	24450007
Optimality of the best value was proved	NO
Number of terms in the objective function	28200
Biggest coefficient in the objective function	41943040
Number of bits for the biggest coefficient in the objective function	26
Sum of the numbers in the objective function	25763487750
Number of bits of the sum of numbers in the objective function	35
Biggest number in a constraint	41943040
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	25763487750
Number of bits of the biggest sum of numbers	35
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.2
Number of variables	37600
Total number of constraints	1090
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1090
Minimum length of a constraint	60
Maximum length of a constraint	480
Trace number 16037

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 06:10:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16328 boxname=wulflinc31 idbench=1256 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c56066a13a725fcc9c143db3d9f8cc06  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-sctap2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-sctap2.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-sctap2.opb
IDLAUNCH: 16328
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        722080 kB
Buffers:         28340 kB
Cached:         255904 kB
SwapCached:        540 kB
Active:         110324 kB
Inactive:       175920 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        721828 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20568 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:30:15 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 16328 7 1200.34 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1503 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssss
c ---[1507]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1506]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1505]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1504]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1503]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1502]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1501]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1500]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1499]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1498]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1497]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1496]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1495]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1494]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1493]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1492]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1491]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1490]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1489]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1488]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1487]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1486]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1485]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1484]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1483]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1482]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1481]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1480]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1479]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1478]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1477]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1476]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1475]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1474]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1473]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1472]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1471]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1470]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1469]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1468]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1467]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1466]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1465]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1464]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1463]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1462]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1461]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1460]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1459]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1458]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1457]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1456]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1455]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1454]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1453]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1452]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1451]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1450]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1449]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1448]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1447]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1446]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1445]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1444]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1443]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1442]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1441]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1440]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1439]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1438]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1437]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1436]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1435]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1434]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1433]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1432]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1431]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1430]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1429]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1428]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1427]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1426]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1425]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1424]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1423]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1422]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1421]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1420]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1419]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1418]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1417]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1416]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1415]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1414]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1413]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1412]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1411]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1410]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1409]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1408]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1407]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1406]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1405]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1404]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1403]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1402]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1401]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1400]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1399]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1398]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1397]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1396]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1395]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1394]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1393]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1392]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1391]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1390]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1389]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1388]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1387]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1386]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1385]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1384]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1383]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1382]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1381]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1380]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1379]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1378]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1377]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1376]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1375]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1374]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1373]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1372]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1371]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1370]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1369]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1368]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1367]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1366]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1365]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1364]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1363]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1362]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1361]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1360]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1359]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1358]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1357]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1356]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1355]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1354]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1353]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1352]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1351]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1350]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1349]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1348]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1347]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1346]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1345]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1344]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1343]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1342]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1341]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1340]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1339]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1338]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1337]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1336]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1335]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1334]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1333]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1332]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1331]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1330]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1329]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1328]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1327]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1326]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1325]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1324]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1323]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1322]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1321]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1320]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1319]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1318]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1317]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1316]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1315]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1314]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1313]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1312]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1311]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1310]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1309]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1308]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1307]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1306]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1305]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1304]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1303]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1302]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1301]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1300]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1299]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1298]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1297]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1296]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1295]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1294]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1293]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1292]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1291]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1290]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1289]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1288]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1287]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1286]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1285]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1284]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1283]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1282]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1281]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1280]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1279]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1278]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1277]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1276]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1275]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1274]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1273]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1272]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1271]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1270]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1269]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1268]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1267]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1266]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1265]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1264]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1263]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1262]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1261]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1260]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1259]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1258]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1257]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1256]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1255]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1254]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1253]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1252]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1251]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1250]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1249]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1248]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1247]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1246]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1245]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1244]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1243]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1242]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1241]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1240]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1239]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1238]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1237]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1236]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1235]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1234]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1233]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1232]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1231]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1230]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1229]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1228]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1227]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1226]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1225]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1224]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1222]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1221]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1220]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1218]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1217]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1216]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1215]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1214]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1213]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1212]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1211]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1210]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1209]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1208]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1207]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1206]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1205]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1204]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1203]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1202]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1201]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1200]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1199]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1198]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1197]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1196]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1195]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1194]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1193]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1192]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1191]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1190]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1189]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1188]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1187]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1186]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1185]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1184]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1183]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1182]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1181]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1180]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1179]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1178]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1177]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1176]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1175]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1174]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1173]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1172]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1171]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1170]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1169]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1168]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1167]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1166]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1165]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1163]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1162]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1161]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1160]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1158]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1157]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1156]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1155]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1154]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1153]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1152]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1151]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1150]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1149]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1148]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1147]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1145]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1144]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1143]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1142]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1141]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1140]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1139]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1138]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1137]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1136]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1134]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1133]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1132]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1130]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1129]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1128]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1127]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1126]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1125]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1124]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1123]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1122]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1121]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1120]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1119]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1118]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1117]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1116]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1115]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1114]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1113]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1112]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1111]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1110]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1109]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1108]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1107]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1106]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1105]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1103]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1102]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1101]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1100]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1099]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1098]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1097]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1096]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1095]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1094]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1093]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1092]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1091]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1090]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1089]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1088]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1087]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1086]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1085]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1083]---> BDD-cost:   76
c ---[1081]---> BDD-cost:   76
c ---[1079]---> BDD-cost:   76
c ---[1077]---> BDD-cost:   76
c ---[1075]---> BDD-cost:   76
c ---[1073]---> BDD-cost:   76
c ---[1071]---> BDD-cost:   76
c ---[1069]---> BDD-cost:   76
c ---[1067]---> BDD-cost:   76
c ---[1065]---> BDD-cost:   76
c ---[1063]---> BDD-cost:   76
c ---[1061]---> BDD-cost:   76
c ---[1059]---> BDD-cost:   76
c ---[1057]---> BDD-cost:   76
c ---[1055]---> BDD-cost:   76
c ---[1053]---> BDD-cost:   76
c ---[1051]---> BDD-cost:   76
c ---[1049]---> BDD-cost:   76
c ---[1047]---> BDD-cost:   76
c ---[1045]---> BDD-cost:   76
c ---[1043]---> BDD-cost:   76
c ---[1041]---> BDD-cost:   76
c ---[1039]---> BDD-cost:   76
c ---[1037]---> BDD-cost:   76
c ---[1035]---> BDD-cost:   76
c ---[1033]---> BDD-cost:   76
c ---[1031]---> BDD-cost:   76
c ---[1029]---> BDD-cost:   76
c ---[1027]---> BDD-cost:   76
c ---[1025]---> BDD-cost:   76
c ---[1023]---> BDD-cost:   76
c ---[1021]---> BDD-cost:   76
c ---[1019]---> BDD-cost:   76
c ---[1017]---> BDD-cost:   76
c ---[1015]---> BDD-cost:   76
c ---[1013]---> BDD-cost:   76
c ---[1011]---> BDD-cost:   76
c ---[1009]---> BDD-cost:   76
c ---[1007]---> BDD-cost:   76
c ---[1005]---> BDD-cost:   76
c ---[1003]---> BDD-cost:   76
c ---[1001]---> BDD-cost:   76
c ---[ 999]---> BDD-cost:   76
c ---[ 997]---> BDD-cost:   76
c ---[ 995]---> BDD-cost:   76
c ---[ 993]---> BDD-cost:   76
c ---[ 991]---> BDD-cost:   76
c ---[ 989]---> BDD-cost:   76
c ---[ 987]---> BDD-cost:   76
c ---[ 985]---> BDD-cost:   76
c ---[ 983]---> BDD-cost:   76
c ---[ 981]---> BDD-cost:   76
c ---[ 979]---> BDD-cost:   76
c ---[ 977]---> BDD-cost:   76
c ---[ 975]---> BDD-cost:   76
c ---[ 973]---> BDD-cost:   76
c ---[ 971]---> BDD-cost:   76
c ---[ 969]---> BDD-cost:   76
c ---[ 967]---> BDD-cost:   76
c ---[ 965]---> BDD-cost:   76
c ---[ 963]---> BDD-cost:   76
c ---[ 961]---> BDD-cost:   76
c ---[ 959]---> BDD-cost:   76
c ---[ 957]---> BDD-cost:   76
c ---[ 955]---> BDD-cost:   76
c ---[ 953]---> BDD-cost:   76
c ---[ 951]---> BDD-cost:   76
c ---[ 949]---> BDD-cost:   76
c ---[ 947]---> BDD-cost:   76
c ---[ 945]---> BDD-cost:   76
c ---[ 943]---> BDD-cost:   76
c ---[ 941]---> BDD-cost:   76
c ---[ 939]---> BDD-cost:   76
c ---[ 937]---> BDD-cost:   76
c ---[ 935]---> BDD-cost:   76
c ---[ 933]---> BDD-cost:   76
c ---[ 931]---> BDD-cost:   76
c ---[ 929]---> BDD-cost:   76
c ---[ 927]---> BDD-cost:   76
c ---[ 925]---> BDD-cost:   76
c ---[ 923]---> BDD-cost:   76
c ---[ 921]---> BDD-cost:   76
c ---[ 919]---> BDD-cost:   76
c ---[ 917]---> BDD-cost:   76
c ---[ 915]---> BDD-cost:   76
c ---[ 913]---> BDD-cost:   76
c ---[ 911]---> BDD-cost:   76
c ---[ 909]---> BDD-cost:   76
c ---[ 907]---> BDD-cost:   76
c ---[ 905]---> BDD-cost:   76
c ---[ 903]---> BDD-cost:   76
c ---[ 901]---> BDD-cost:   76
c ---[ 899]---> BDD-cost:   76
c ---[ 897]---> BDD-cost:   76
c ---[ 895]---> BDD-cost:   76
c ---[ 893]---> BDD-cost:   76
c ---[ 891]---> BDD-cost:   76
c ---[ 889]---> BDD-cost:   76
c ---[ 887]---> BDD-cost:   76
c ---[ 885]---> BDD-cost:   76
c ---[ 883]---> BDD-cost:   76
c ---[ 881]---> BDD-cost:   76
c ---[ 879]---> BDD-cost:   76
c ---[ 877]---> BDD-cost:   76
c ---[ 875]---> BDD-cost:   76
c ---[ 873]---> BDD-cost:   76
c ---[ 871]---> BDD-cost:   76
c ---[ 869]---> BDD-cost:   76
c ---[ 867]---> BDD-cost:   76
c ---[ 865]---> BDD-cost:   76
c ---[ 863]---> BDD-cost:   76
c ---[ 861]---> BDD-cost:   76
c ---[ 859]---> BDD-cost:   76
c ---[ 857]---> BDD-cost:   76
c ---[ 855]---> BDD-cost:   76
c ---[ 853]---> BDD-cost:   76
c ---[ 851]---> BDD-cost:   76
c ---[ 849]---> BDD-cost:   76
c ---[ 847]---> BDD-cost:   76
c ---[ 845]---> BDD-cost:   76
c ---[ 843]---> BDD-cost:   76
c ---[ 841]---> BDD-cost:   76
c ---[ 839]---> BDD-cost:   76
c ---[ 837]---> BDD-cost:   76
c ---[ 835]---> BDD-cost:   76
c ---[ 833]---> BDD-cost:   76
c ---[ 831]---> BDD-cost:   76
c ---[ 829]---> BDD-cost:   76
c ---[ 827]---> BDD-cost:   76
c ---[ 825]---> BDD-cost:   76
c ---[ 823]---> BDD-cost:   76
c ---[ 821]---> BDD-cost:   76
c ---[ 819]---> BDD-cost:   76
c ---[ 817]---> BDD-cost:   76
c ---[ 815]---> BDD-cost:   76
c ---[ 813]---> BDD-cost:   76
c ---[ 811]---> BDD-cost:   76
c ---[ 809]---> BDD-cost:   76
c ---[ 807]---> BDD-cost:   76
c ---[ 805]---> BDD-cost:   76
c ---[ 803]---> BDD-cost:   76
c ---[ 801]---> BDD-cost:   76
c ---[ 799]---> BDD-cost:   76
c ---[ 797]---> BDD-cost:   76
c ---[ 795]---> BDD-cost:   76
c ---[ 793]---> BDD-cost:   76
c ---[ 791]---> BDD-cost:   76
c ---[ 789]---> BDD-cost:   76
c ---[ 787]---> BDD-cost:   76
c ---[ 785]---> BDD-cost:   76
c ---[ 783]---> BDD-cost:   76
c ---[ 781]---> BDD-cost:   76
c ---[ 779]---> BDD-cost:   76
c ---[ 777]---> BDD-cost:   76
c ---[ 775]---> BDD-cost:   76
c ---[ 773]---> BDD-cost:   76
c ---[ 771]---> BDD-cost:   76
c ---[ 769]---> BDD-cost:   76
c ---[ 767]---> BDD-cost:   76
c ---[ 765]---> BDD-cost:   76
c ---[ 763]---> BDD-cost:   76
c ---[ 761]---> BDD-cost:   76
c ---[ 759]---> BDD-cost:   76
c ---[ 757]---> BDD-cost:   76
c ---[ 755]---> BDD-cost:   76
c ---[ 753]---> BDD-cost:   76
c ---[ 751]---> BDD-cost:   76
c ---[ 749]---> BDD-cost:   76
c ---[ 747]---> BDD-cost:   76
c ---[ 745]---> BDD-cost:   76
c ---[ 743]---> BDD-cost:   76
c ---[ 741]---> BDD-cost:   76
c ---[ 739]---> BDD-cost:   76
c ---[ 737]---> BDD-cost:   76
c ---[ 735]---> BDD-cost:   76
c ---[ 733]---> BDD-cost:   76
c ---[ 731]---> BDD-cost:   76
c ---[ 729]---> BDD-cost:   76
c ---[ 727]---> BDD-cost:   76
c ---[ 725]---> BDD-cost:   76
c ---[ 723]---> BDD-cost:   76
c ---[ 721]---> BDD-cost:   76
c ---[ 719]---> BDD-cost:   76
c ---[ 717]---> BDD-cost:   76
c ---[ 715]---> BDD-cost:   76
c ---[ 713]---> BDD-cost:   76
c ---[ 711]---> BDD-cost:   76
c ---[ 709]---> BDD-cost:   76
c ---[ 707]---> BDD-cost:   76
c ---[ 705]---> BDD-cost:   76
c ---[ 703]---> BDD-cost:   76
c ---[ 701]---> BDD-cost:   76
c ---[ 699]---> BDD-cost:   76
c ---[ 697]---> BDD-cost:   76
c ---[ 695]---> BDD-cost:   76
c ---[ 693]---> BDD-cost:   76
c ---[ 691]---> BDD-cost:   76
c ---[ 689]---> BDD-cost:   76
c ---[ 687]---> BDD-cost:   76
c ---[ 685]---> BDD-cost:   76
c ---[ 683]---> BDD-cost:   76
c ---[ 681]---> BDD-cost:   76
c ---[ 679]---> BDD-cost:   76
c ---[ 677]---> BDD-cost:   76
c ---[ 675]---> BDD-cost:   76
c ---[ 673]---> BDD-cost:   76
c ---[ 671]---> BDD-cost:   76
c ---[ 669]---> BDD-cost:   76
c ---[ 667]---> BDD-cost:   76
c ---[ 665]---> BDD-cost:   76
c ---[ 663]---> BDD-cost:   74
c ---[ 661]---> BDD-cost:   76
c ---[ 659]---> BDD-cost:   74
c ---[ 657]---> BDD-cost:   74
c ---[ 655]---> BDD-cost:   74
c ---[ 653]---> BDD-cost:   74
c ---[ 651]---> BDD-cost:   74
c ---[ 649]---> BDD-cost:   74
c ---[ 647]---> BDD-cost:   74
c ---[ 645]---> BDD-cost:   74
c ---[ 643]---> BDD-cost:   74
c ---[ 641]---> BDD-cost:   76
c ---[ 639]---> BDD-cost:   74
c ---[ 637]---> BDD-cost:   74
c ---[ 635]---> BDD-cost:   74
c ---[ 633]---> BDD-cost:   74
c ---[ 631]---> BDD-cost:   74
c ---[ 629]---> BDD-cost:   74
c ---[ 627]---> BDD-cost:   74
c ---[ 625]---> BDD-cost:   74
c ---[ 623]---> BDD-cost:   74
c ---[ 621]---> BDD-cost:   76
c ---[ 619]---> BDD-cost:   74
c ---[ 617]---> BDD-cost:   74
c ---[ 615]---> BDD-cost:   74
c ---[ 613]---> BDD-cost:   74
c ---[ 611]---> BDD-cost:   74
c ---[ 609]---> BDD-cost:   74
c ---[ 607]---> BDD-cost:   74
c ---[ 605]---> BDD-cost:   74
c ---[ 603]---> BDD-cost:   74
c ---[ 601]---> BDD-cost:   76
c ---[ 599]---> BDD-cost:   74
c ---[ 597]---> BDD-cost:   74
c ---[ 595]---> BDD-cost:   74
c ---[ 593]---> BDD-cost:   74
c ---[ 591]---> BDD-cost:   74
c ---[ 589]---> BDD-cost:   74
c ---[ 587]---> BDD-cost:   74
c ---[ 585]---> BDD-cost:   74
c ---[ 583]---> BDD-cost:   74
c ---[ 581]---> BDD-cost:   76
c ---[ 579]---> BDD-cost:   74
c ---[ 577]---> BDD-cost:   74
c ---[ 575]---> BDD-cost:   74
c ---[ 573]---> BDD-cost:   74
c ---[ 571]---> BDD-cost:   74
c ---[ 569]---> BDD-cost:   74
c ---[ 567]---> BDD-cost:   74
c ---[ 565]---> BDD-cost:   74
c ---[ 563]---> BDD-cost:   74
c ---[ 561]---> BDD-cost:   76
c ---[ 559]---> BDD-cost:   74
c ---[ 557]---> BDD-cost:   74
c ---[ 555]---> BDD-cost:   74
c ---[ 553]---> BDD-cost:   74
c ---[ 551]---> BDD-cost:   74
c ---[ 549]---> BDD-cost:   74
c ---[ 547]---> BDD-cost:   74
c ---[ 545]---> BDD-cost:   74
c ---[ 543]---> BDD-cost:   74
c ---[ 541]---> BDD-cost:   76
c ---[ 539]---> BDD-cost:   74
c ---[ 537]---> BDD-cost:   74
c ---[ 535]---> BDD-cost:   74
c ---[ 533]---> BDD-cost:   74
c ---[ 531]---> BDD-cost:   74
c ---[ 529]---> BDD-cost:   74
c ---[ 527]---> BDD-cost:   74
c ---[ 525]---> BDD-cost:   74
c ---[ 523]---> BDD-cost:   74
c ---[ 521]---> BDD-cost:   76
c ---[ 519]---> BDD-cost:   74
c ---[ 517]---> BDD-cost:   74
c ---[ 515]---> BDD-cost:   74
c ---[ 513]---> BDD-cost:   74
c ---[ 511]---> BDD-cost:   74
c ---[ 509]---> BDD-cost:   74
c ---[ 507]---> BDD-cost:   74
c ---[ 505]---> BDD-cost:   74
c ---[ 503]---> BDD-cost:   74
c ---[ 501]---> BDD-cost:   76
c ---[ 499]---> BDD-cost:   74
c ---[ 497]---> BDD-cost:   74
c ---[ 495]---> BDD-cost:   74
c ---[ 493]---> BDD-cost:   74
c ---[ 491]---> BDD-cost:   74
c ---[ 489]---> BDD-cost:   74
c ---[ 487]---> BDD-cost:   74
c ---[ 485]---> BDD-cost:   74
c ---[ 483]---> BDD-cost:   74
c ---[ 481]---> BDD-cost:   76
c ---[ 479]---> BDD-cost:   74
c ---[ 477]---> BDD-cost:   74
c ---[ 475]---> BDD-cost:   74
c ---[ 473]---> BDD-cost:   74
c ---[ 471]---> BDD-cost:   74
c ---[ 469]---> BDD-cost:   74
c ---[ 467]---> BDD-cost:   74
c ---[ 465]---> BDD-cost:   74
c ---[ 463]---> BDD-cost:   74
c ---[ 461]---> BDD-cost:   76
c ---[ 459]---> BDD-cost:   74
c ---[ 457]---> BDD-cost:   74
c ---[ 455]---> BDD-cost:   74
c ---[ 453]---> BDD-cost:   74
c ---[ 451]---> BDD-cost:   74
c ---[ 449]---> BDD-cost:   74
c ---[ 447]---> BDD-cost:   74
c ---[ 445]---> BDD-cost:   74
c ---[ 443]---> BDD-cost:   74
c ---[ 441]---> BDD-cost:   76
c ---[ 439]---> BDD-cost:   74
c ---[ 437]---> BDD-cost:   74
c ---[ 435]---> BDD-cost:   74
c ---[ 433]---> BDD-cost:   74
c ---[ 431]---> BDD-cost:   74
c ---[ 429]---> BDD-cost:   74
c ---[ 427]---> BDD-cost:   74
c ---[ 425]---> BDD-cost:   74
c ---[ 423]---> BDD-cost:   74
c ---[ 421]---> BDD-cost:   76
c ---[ 419]---> BDD-cost:   74
c ---[ 417]---> BDD-cost:   74
c ---[ 415]---> BDD-cost:   74
c ---[ 413]---> BDD-cost:   74
c ---[ 411]---> BDD-cost:   74
c ---[ 409]---> BDD-cost:   74
c ---[ 407]---> BDD-cost:   74
c ---[ 405]---> BDD-cost:   74
c ---[ 403]---> BDD-cost:   74
c ---[ 401]---> BDD-cost:   76
c ---[ 399]---> BDD-cost:   74
c ---[ 397]---> BDD-cost:   74
c ---[ 395]---> BDD-cost:   74
c ---[ 393]---> BDD-cost:   74
c ---[ 391]---> BDD-cost:   74
c ---[ 389]---> BDD-cost:   74
c ---[ 387]---> BDD-cost:   74
c ---[ 385]---> BDD-cost:   74
c ---[ 383]---> BDD-cost:   76
c ---[ 381]---> BDD-cost:   76
c ---[ 379]---> BDD-cost:   76
c ---[ 377]---> BDD-cost:   76
c ---[ 375]---> BDD-cost:   76
c ---[ 373]---> BDD-cost:   76
c ---[ 371]---> BDD-cost:   76
c ---[ 369]---> BDD-cost:   76
c ---[ 367]---> BDD-cost:   76
c ---[ 365]---> BDD-cost:   76
c ---[ 363]---> BDD-cost:   76
c ---[ 361]---> BDD-cost:   76
c ---[ 359]---> BDD-cost:   76
c ---[ 357]---> BDD-cost:   76
c ---[ 355]---> BDD-cost:   76
c ---[ 353]---> BDD-cost:   76
c ---[ 351]---> BDD-cost:   76
c ---[ 349]---> BDD-cost:   76
c ---[ 347]---> BDD-cost:   76
c ---[ 345]---> BDD-cost:   76
c ---[ 343]---> BDD-cost:   76
c ---[ 341]---> BDD-cost:   76
c ---[ 339]---> BDD-cost:   76
c ---[ 337]---> BDD-cost:   76
c ---[ 335]---> BDD-cost:   76
c ---[ 333]---> BDD-cost:   76
c ---[ 331]---> BDD-cost:   76
c ---[ 329]---> BDD-cost:   76
c ---[ 327]---> BDD-cost:   76
c ---[ 325]---> BDD-cost:   76
c ---[ 323]---> BDD-cost:   76
c ---[ 321]---> BDD-cost:   76
c ---[ 319]---> BDD-cost:   76
c ---[ 317]---> BDD-cost:   76
c ---[ 315]---> BDD-cost:   76
c ---[ 313]---> BDD-cost:   76
c ---[ 311]---> BDD-cost:   76
c ---[ 309]---> BDD-cost:   76
c ---[ 307]---> BDD-cost:   76
c ---[ 305]---> BDD-cost:   76
c ---[ 303]---> BDD-cost:   76
c ---[ 301]---> BDD-cost:   76
c ---[ 299]---> BDD-cost:   76
c ---[ 297]---> BDD-cost:   76
c ---[ 295]---> BDD-cost:   76
c ---[ 293]---> BDD-cost:   76
c ---[ 291]---> BDD-cost:   76
c ---[ 289]---> BDD-cost:   76
c ---[ 287]---> BDD-cost:   76
c ---[ 285]---> BDD-cost:   76
c ---[ 283]---> BDD-cost:   76
c ---[ 281]---> BDD-cost:   76
c ---[ 279]---> BDD-cost:   76
c ---[ 277]---> BDD-cost:   76
c ---[ 275]---> BDD-cost:   76
c ---[ 273]---> BDD-cost:   76
c ---[ 271]---> BDD-cost:   76
c ---[ 269]---> BDD-cost:   76
c ---[ 267]---> BDD-cost:   76
c ---[ 265]---> BDD-cost:   76
c ---[ 263]---> BDD-cost:   76
c ---[ 261]---> BDD-cost:   76
c ---[ 259]---> BDD-cost:   76
c ---[ 257]---> BDD-cost:   76
c ---[ 255]---> BDD-cost:   76
c ---[ 253]---> BDD-cost:   76
c ---[ 251]---> BDD-cost:   76
c ---[ 249]---> BDD-cost:   76
c ---[ 247]---> BDD-cost:   76
c ---[ 245]---> BDD-cost:   76
c ---[ 243]---> BDD-cost:   76
c ---[ 241]---> BDD-cost:   76
c ---[ 239]---> BDD-cost:   76
c ---[ 237]---> BDD-cost:   76
c ---[ 235]---> BDD-cost:   76
c ---[ 233]---> BDD-cost:   76
c ---[ 231]---> BDD-cost:   76
c ---[ 229]---> BDD-cost:   76
c ---[ 227]---> BDD-cost:   76
c ---[ 225]---> BDD-cost:   76
c ---[ 223]---> BDD-cost:   76
c ---[ 221]---> BDD-cost:   76
c ---[ 219]---> BDD-cost:   76
c ---[ 217]---> BDD-cost:   76
c ---[ 215]---> BDD-cost:   76
c ---[ 213]---> BDD-cost:   76
c ---[ 211]---> BDD-cost:   76
c ---[ 209]---> BDD-cost:   76
c ---[ 207]---> BDD-cost:   76
c ---[ 205]---> BDD-cost:   76
c ---[ 203]---> BDD-cost:   76
c ---[ 201]---> BDD-cost:   76
c ---[ 199]---> BDD-cost:   76
c ---[ 197]---> BDD-cost:   76
c ---[ 195]---> BDD-cost:   76
c ---[ 193]---> BDD-cost:   76
c ---[ 191]---> BDD-cost:   76
c ---[ 189]---> BDD-cost:   76
c ---[ 187]---> BDD-cost:   76
c ---[ 185]---> BDD-cost:   76
c ---[ 183]---> BDD-cost:   76
c ---[ 181]---> BDD-cost:   76
c ---[ 179]---> BDD-cost:   76
c ---[ 177]---> BDD-cost:   76
c ---[ 175]---> BDD-cost:   76
c ---[ 173]---> BDD-cost:   76
c ---[ 171]---> BDD-cost:   76
c ---[ 169]---> BDD-cost:   76
c ---[ 167]---> BDD-cost:   76
c ---[ 165]---> BDD-cost:   76
c ---[ 163]---> BDD-cost:   76
c ---[ 161]---> BDD-cost:   76
c ---[ 159]---> BDD-cost:   76
c ---[ 157]---> BDD-cost:   76
c ---[ 155]---> BDD-cost:   76
c ---[ 153]---> BDD-cost:   76
c ---[ 151]---> BDD-cost:   76
c ---[ 149]---> BDD-cost:   76
c ---[ 147]---> BDD-cost:   76
c ---[ 145]---> BDD-cost:   76
c ---[ 144]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 143]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 142]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 141]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 140]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 139]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 138]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 137]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 136]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[ 135]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 134]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 133]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 132]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 131]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 130]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 129]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 128]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 127]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 126]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 125]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 124]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 123]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 122]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 121]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 120]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 119]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 118]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[ 117]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 115]---> Adder-cost: 974   maxlim: 4217009   bits: 24/23
c ---[ 114]---> Adder-cost: 972   maxlim: 4218289   bits: 24/23
c ---[ 113]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[ 112]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[ 111]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 110]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 109]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 108]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[ 107]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 106]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 105]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 104]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 103]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 102]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 101]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 100]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[  99]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[  98]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  96]---> Adder-cost: 974   maxlim: 4214449   bits: 24/23
c ---[  95]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  94]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  93]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  92]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  91]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  90]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  89]---> Adder-cost: 970   maxlim: 4213809   bits: 24/23
c ---[  88]---> Adder-cost: 714   maxlim: 3162809   bits: 23/22
c ---[  86]---> Adder-cost: 714   maxlim: 3164089   bits: 23/22
c ---[  85]---> Adder-cost: 674   maxlim: 3164729   bits: 23/22
c ---[  84]---> Adder-cost: 674   maxlim: 3165369   bits: 23/22
c ---[  83]---> Adder-cost: 674   maxlim: 3165369   bits: 23/22
c ---[  82]---> Adder-cost: 674   maxlim: 3165369   bits: 23/22
c ---[  81]---> Adder-cost: 674   maxlim: 3164089   bits: 23/22
c ---[  80]---> Adder-cost: 674   maxlim: 3164089   bits: 23/22
c ---[  79]---> Adder-cost: 634   maxlim: 3162809   bits: 23/22
c ---[  78]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  76]---> Adder-cost: 974   maxlim: 4213809   bits: 24/23
c ---[  75]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  74]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  73]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  72]---> Adder-cost: 972   maxlim: 4215089   bits: 24/23
c ---[  71]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  70]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[  69]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[  68]---> Adder-cost: 714   maxlim: 3162809   bits: 23/22
c ---[  67]---> Adder-cost: 714   maxlim: 3163449   bits: 23/22
c ---[  66]---> Adder-cost: 674   maxlim: 3164089   bits: 23/22
c ---[  65]---> Adder-cost: 674   maxlim: 3165369   bits: 23/22
c ---[  64]---> Adder-cost: 674   maxlim: 3166649   bits: 23/22
c ---[  63]---> Adder-cost: 674   maxlim: 3164089   bits: 23/22
c ---[  62]---> Adder-cost: 674   maxlim: 3163449   bits: 23/22
c ---[  61]---> Adder-cost: 674   maxlim: 3162809   bits: 23/22
c ---[  60]---> Adder-cost: 634   maxlim: 3162809   bits: 23/22
c ---[  59]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[  58]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[  57]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  56]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  55]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  54]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  53]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  52]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  51]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[  50]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  49]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  48]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  47]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  46]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  45]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  44]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  43]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  42]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  41]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  40]---> Adder-cost: 974   maxlim: 4214449   bits: 24/23
c ---[  39]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  38]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  37]---> Adder-cost: 972   maxlim: 4219569   bits: 24/23
c ---[  36]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  35]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  34]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  33]---> Adder-cost: 970   maxlim: 4213809   bits: 24/23
c ---[  32]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  31]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  30]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  29]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  28]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  27]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  26]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  25]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  24]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  23]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  22]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  21]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  20]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  19]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  18]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  17]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  16]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  15]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  14]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  12]---> Adder-cost: 974   maxlim: 4213809   bits: 24/23
c ---[  11]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[  10]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   9]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[   8]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   7]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   6]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[   5]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[   4]---> Adder-cost: 333   maxlim: 1279   bits: 12/11
c ---[   3]---> Adder-cost: 333   maxlim: 1279   bits: 12/11
c ---[   2]---> Adder-cost: 186   maxlim: 639   bits: 11/10
c ---[   1]---> Adder-cost: 287   maxlim: 639   bits: 11/10
c ---[   0]---> Adder-cost: 287   maxlim: 639   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2977810  8088744 |  992603       0        0     nan |  0.000 % |
c |       100 | 2977810  8088744 | 1091863     100      327     3.3 |  2.269 % |
c |       250 | 2977810  8088744 | 1201049     250      950     3.8 |  2.269 % |
c |       475 | 2977810  8088744 | 1321154     475     2173     4.6 |  2.269 % |
c |       814 | 2977734  8088575 | 1453270     812     3686     4.5 |  2.272 % |
c |      1320 | 2977734  8088575 | 1598597    1318     6409     4.9 |  2.272 % |
c |      2079 | 2977673  8088439 | 1758456    2076    11025     5.3 |  2.273 % |
c |      3218 | 2977673  8088439 | 1934302    3215    19203     6.0 |  2.273 % |
c |      4926 | 2977633  8088350 | 2127732    4922    29365     6.0 |  2.275 % |
c |      7488 | 2977534  8088130 | 2340505    7479    43204     5.8 |  2.278 % |
c |     11333 | 2977362  8087749 | 2574556   11317    75371     6.7 |  2.283 % |
c |     17102 | 2977191  8087369 | 2832012   17081   118710     6.9 |  2.288 % |
c |     25751 | 2976426  8085661 | 3115213   25702   183777     7.2 |  2.312 % |
c |     38727 | 2975764  8084186 | 3426734   38656   324498     8.4 |  2.332 % |
c |     58190 | 2974776  8081986 | 3769408   58074   492652     8.5 |  2.362 % |
c |     87382 | 2972161  8076140 | 4146349   87176   760576     8.7 |  2.444 % |
c |    131171 | 2967270  8065204 | 4560983  130766  1190985     9.1 |  2.596 % |
#### 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.91 0.95 0.90 2/54 23106
Raw data (stat): 23106 (runsolver) R 23105 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542797295 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 14781 0 0 0 959 39 0 0 25 0 1 0 542797295 54411264 11941 4294967295 134512640 134672761 3221224544 3221223248 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13284 11941 603 41 0 13243 0
vsize: 53136
[startup+20.0007 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 51002 0 0 0 1875 123 0 0 25 0 1 0 542797295 235778048 48162 4294967295 134512640 134672761 3221224544 3221204272 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57563 48164 603 41 0 57522 0
vsize: 230252
[startup+30.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 72517 0 0 0 2824 174 0 0 25 0 1 0 542797295 311308288 69677 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76003 69677 603 41 0 75962 0
vsize: 304012
[startup+40.0016 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 72667 0 0 0 3822 175 0 0 25 0 1 0 542797295 311853056 69827 4294967295 134512640 134672761 3221224544 3221223712 134564798 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76136 69827 603 41 0 76095 0
vsize: 304544
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 72816 0 0 0 4821 176 0 0 25 0 1 0 542797295 312262656 69976 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76236 69976 603 41 0 76195 0
vsize: 304944
[startup+60.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 72906 0 0 0 5821 176 0 0 25 0 1 0 542797295 312594432 70066 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76317 70066 603 41 0 76276 0
vsize: 305268
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 72970 0 0 0 6821 176 0 0 25 0 1 0 542797295 312864768 70130 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76383 70130 603 41 0 76342 0
vsize: 305532
[startup+80.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73006 0 0 0 7820 177 0 0 25 0 1 0 542797295 312999936 70166 4294967295 134512640 134672761 3221224544 3221223728 134559452 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76416 70166 603 41 0 76375 0
vsize: 305664
[startup+90.0021 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73073 0 0 0 8819 177 0 0 25 0 1 0 542797295 313135104 70233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76449 70233 603 41 0 76408 0
vsize: 305796
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73100 0 0 0 9819 177 0 0 25 0 1 0 542797295 313270272 70260 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76482 70260 603 41 0 76441 0
vsize: 305928
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73148 0 0 0 10819 177 0 0 25 0 1 0 542797295 313499648 70308 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76538 70308 603 41 0 76497 0
vsize: 306152
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73242 0 0 0 11819 177 0 0 25 0 1 0 542797295 313769984 70402 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76604 70402 603 41 0 76563 0
vsize: 306416
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73300 0 0 0 12819 178 0 0 25 0 1 0 542797295 314040320 70460 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76670 70460 603 41 0 76629 0
vsize: 306680
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73346 0 0 0 13819 178 0 0 25 0 1 0 542797295 314175488 70506 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76703 70506 603 41 0 76662 0
vsize: 306812
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73408 0 0 0 14819 178 0 0 25 0 1 0 542797295 314445824 70568 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76769 70568 603 41 0 76728 0
vsize: 307076
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73448 0 0 0 15819 178 0 0 25 0 1 0 542797295 314580992 70608 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76802 70608 603 41 0 76761 0
vsize: 307208
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73481 0 0 0 16819 178 0 0 25 0 1 0 542797295 314716160 70641 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76835 70641 603 41 0 76794 0
vsize: 307340
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73504 0 0 0 17819 178 0 0 25 0 1 0 542797295 314716160 70664 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76835 70664 603 41 0 76794 0
vsize: 307340
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73646 0 0 0 18819 179 0 0 25 0 1 0 542797295 315256832 70806 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76967 70806 603 41 0 76926 0
vsize: 307868
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73693 0 0 0 19819 179 0 0 25 0 1 0 542797295 315392000 70853 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77000 70853 603 41 0 76959 0
vsize: 308000
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73754 0 0 0 20819 179 0 0 25 0 1 0 542797295 315789312 70914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77097 70914 603 41 0 77056 0
vsize: 308388
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73827 0 0 0 21818 180 0 0 25 0 1 0 542797295 316059648 70987 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77163 70987 603 41 0 77122 0
vsize: 308652
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73858 0 0 0 22818 180 0 0 25 0 1 0 542797295 316194816 71018 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77196 71018 603 41 0 77155 0
vsize: 308784
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73888 0 0 0 23818 180 0 0 25 0 1 0 542797295 316194816 71048 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77196 71048 603 41 0 77155 0
vsize: 308784
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73917 0 0 0 24818 180 0 0 25 0 1 0 542797295 316329984 71077 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77229 71077 603 41 0 77188 0
vsize: 308916
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73937 0 0 0 25819 180 0 0 25 0 1 0 542797295 316465152 71097 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77262 71097 603 41 0 77221 0
vsize: 309048
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73956 0 0 0 26819 181 0 0 25 0 1 0 542797295 316465152 71116 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77262 71116 603 41 0 77221 0
vsize: 309048
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73977 0 0 0 27819 181 0 0 25 0 1 0 542797295 316600320 71137 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77295 71137 603 41 0 77254 0
vsize: 309180
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 73994 0 0 0 28819 181 0 0 25 0 1 0 542797295 316600320 71154 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77295 71154 603 41 0 77254 0
vsize: 309180
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74024 0 0 0 29819 181 0 0 25 0 1 0 542797295 316735488 71184 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77328 71184 603 41 0 77287 0
vsize: 309312
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74132 0 0 0 30819 181 0 0 25 0 1 0 542797295 317140992 71292 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77427 71292 603 41 0 77386 0
vsize: 309708
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74151 0 0 0 31818 182 0 0 25 0 1 0 542797295 317140992 71311 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77427 71311 603 41 0 77386 0
vsize: 309708
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74177 0 0 0 32818 182 0 0 25 0 1 0 542797295 317276160 71337 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77460 71337 603 41 0 77419 0
vsize: 309840
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74220 0 0 0 33818 182 0 0 25 0 1 0 542797295 317411328 71380 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77493 71380 603 41 0 77452 0
vsize: 309972
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74277 0 0 0 34818 183 0 0 25 0 1 0 542797295 317681664 71437 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77559 71437 603 41 0 77518 0
vsize: 310236
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74400 0 0 0 35818 183 0 0 25 0 1 0 542797295 318087168 71560 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77658 71560 603 41 0 77617 0
vsize: 310632
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74443 0 0 0 36818 183 0 0 25 0 1 0 542797295 318222336 71603 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77691 71603 603 41 0 77650 0
vsize: 310764
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74471 0 0 0 37817 183 0 0 25 0 1 0 542797295 318357504 71631 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77724 71631 603 41 0 77683 0
vsize: 310896
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74503 0 0 0 38817 183 0 0 25 0 1 0 542797295 318492672 71663 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77757 71663 603 41 0 77716 0
vsize: 311028
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74538 0 0 0 39817 183 0 0 25 0 1 0 542797295 318627840 71698 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77790 71698 603 41 0 77749 0
vsize: 311160
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74575 0 0 0 40818 183 0 0 25 0 1 0 542797295 318763008 71735 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77823 71735 603 41 0 77782 0
vsize: 311292
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74684 0 0 0 41817 184 0 0 25 0 1 0 542797295 319430656 71844 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77986 71844 603 41 0 77945 0
vsize: 311944
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74704 0 0 0 42817 184 0 0 25 0 1 0 542797295 319565824 71864 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78019 71864 603 41 0 77978 0
vsize: 312076
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74723 0 0 0 43817 184 0 0 25 0 1 0 542797295 319565824 71883 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78019 71883 603 41 0 77978 0
vsize: 312076
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74743 0 0 0 44818 184 0 0 25 0 1 0 542797295 319700992 71903 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78052 71903 603 41 0 78011 0
vsize: 312208
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74769 0 0 0 45818 185 0 0 25 0 1 0 542797295 319836160 71929 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78085 71929 603 41 0 78044 0
vsize: 312340
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74795 0 0 0 46817 185 0 0 25 0 1 0 542797295 319836160 71955 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78085 71955 603 41 0 78044 0
vsize: 312340
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74813 0 0 0 47817 185 0 0 25 0 1 0 542797295 319971328 71973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78118 71973 603 41 0 78077 0
vsize: 312472
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74835 0 0 0 48817 185 0 0 25 0 1 0 542797295 320106496 71995 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78151 71995 603 41 0 78110 0
vsize: 312604
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74850 0 0 0 49817 186 0 0 25 0 1 0 542797295 320106496 72010 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78151 72010 603 41 0 78110 0
vsize: 312604
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74878 0 0 0 50817 186 0 0 25 0 1 0 542797295 320241664 72038 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78184 72038 603 41 0 78143 0
vsize: 312736
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74902 0 0 0 51818 186 0 0 25 0 1 0 542797295 320376832 72062 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78217 72062 603 41 0 78176 0
vsize: 312868
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74929 0 0 0 52817 186 0 0 25 0 1 0 542797295 320376832 72089 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78217 72089 603 41 0 78176 0
vsize: 312868
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74957 0 0 0 53817 186 0 0 25 0 1 0 542797295 320512000 72117 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78250 72117 603 41 0 78209 0
vsize: 313000
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74977 0 0 0 54817 187 0 0 25 0 1 0 542797295 320647168 72137 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78283 72137 603 41 0 78242 0
vsize: 313132
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 74991 0 0 0 55817 187 0 0 25 0 1 0 542797295 320647168 72151 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78283 72151 603 41 0 78242 0
vsize: 313132
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75017 0 0 0 56818 187 0 0 25 0 1 0 542797295 320782336 72177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78316 72177 603 41 0 78275 0
vsize: 313264
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75033 0 0 0 57818 187 0 0 25 0 1 0 542797295 320782336 72193 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78316 72193 603 41 0 78275 0
vsize: 313264
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75051 0 0 0 58818 187 0 0 25 0 1 0 542797295 320917504 72211 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78349 72211 603 41 0 78308 0
vsize: 313396
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75068 0 0 0 59818 187 0 0 25 0 1 0 542797295 320917504 72228 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78349 72228 603 41 0 78308 0
vsize: 313396
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75087 0 0 0 60818 187 0 0 25 0 1 0 542797295 321052672 72247 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78382 72247 603 41 0 78341 0
vsize: 313528
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75103 0 0 0 61818 187 0 0 25 0 1 0 542797295 321052672 72263 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78382 72263 603 41 0 78341 0
vsize: 313528
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75121 0 0 0 62818 187 0 0 25 0 1 0 542797295 321187840 72281 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78415 72281 603 41 0 78374 0
vsize: 313660
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75157 0 0 0 63817 188 0 0 25 0 1 0 542797295 321323008 72317 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78448 72317 603 41 0 78407 0
vsize: 313792
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75191 0 0 0 64816 188 0 0 25 0 1 0 542797295 321458176 72351 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78481 72351 603 41 0 78440 0
vsize: 313924
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75217 0 0 0 65817 189 0 0 25 0 1 0 542797295 321589248 72377 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78513 72377 603 41 0 78472 0
vsize: 314052
[startup+670.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75245 0 0 0 66817 189 0 0 25 0 1 0 542797295 321589248 72405 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78513 72405 603 41 0 78472 0
vsize: 314052
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75254 0 0 0 67817 189 0 0 25 0 1 0 542797295 321724416 72414 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78546 72414 603 41 0 78505 0
vsize: 314184
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75268 0 0 0 68817 189 0 0 25 0 1 0 542797295 321724416 72428 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78546 72428 603 41 0 78505 0
vsize: 314184
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75326 0 0 0 69817 189 0 0 25 0 1 0 542797295 321859584 72486 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78579 72486 603 41 0 78538 0
vsize: 314316
[startup+710.034 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75344 0 0 0 70817 189 0 0 25 0 1 0 542797295 321994752 72504 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78612 72504 603 41 0 78571 0
vsize: 314448
[startup+720.034 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75360 0 0 0 71817 189 0 0 25 0 1 0 542797295 321994752 72520 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78612 72520 603 41 0 78571 0
vsize: 314448
[startup+730.034 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75374 0 0 0 72817 189 0 0 25 0 1 0 542797295 322129920 72534 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78645 72534 603 41 0 78604 0
vsize: 314580
[startup+740.035 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75386 0 0 0 73818 189 0 0 25 0 1 0 542797295 322129920 72546 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78645 72546 603 41 0 78604 0
vsize: 314580
[startup+750.035 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75398 0 0 0 74818 189 0 0 25 0 1 0 542797295 322129920 72558 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78645 72558 603 41 0 78604 0
vsize: 314580
[startup+760.036 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75410 0 0 0 75818 189 0 0 25 0 1 0 542797295 322265088 72570 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78678 72570 603 41 0 78637 0
vsize: 314712
[startup+770.036 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75430 0 0 0 76818 189 0 0 25 0 1 0 542797295 322265088 72590 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78678 72590 603 41 0 78637 0
vsize: 314712
[startup+780.035 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75440 0 0 0 77818 189 0 0 25 0 1 0 542797295 322400256 72600 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78711 72600 603 41 0 78670 0
vsize: 314844
[startup+790.036 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75447 0 0 0 78819 189 0 0 25 0 1 0 542797295 322400256 72607 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78711 72607 603 41 0 78670 0
vsize: 314844
[startup+800.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75459 0 0 0 79819 189 0 0 25 0 1 0 542797295 322400256 72619 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78711 72619 603 41 0 78670 0
vsize: 314844
[startup+810.041 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75473 0 0 0 80819 189 0 0 25 0 1 0 542797295 322535424 72633 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78744 72633 603 41 0 78703 0
vsize: 314976
[startup+820.042 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75488 0 0 0 81819 190 0 0 25 0 1 0 542797295 322535424 72648 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78744 72648 603 41 0 78703 0
vsize: 314976
[startup+830.042 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75506 0 0 0 82819 190 0 0 25 0 1 0 542797295 322535424 72666 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78744 72666 603 41 0 78703 0
vsize: 314976
[startup+840.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75526 0 0 0 83819 190 0 0 25 0 1 0 542797295 322670592 72686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78777 72686 603 41 0 78736 0
vsize: 315108
[startup+850.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75542 0 0 0 84820 190 0 0 25 0 1 0 542797295 322670592 72702 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78777 72702 603 41 0 78736 0
vsize: 315108
[startup+860.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75561 0 0 0 85820 190 0 0 25 0 1 0 542797295 322805760 72721 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78810 72721 603 41 0 78769 0
vsize: 315240
[startup+870.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75575 0 0 0 86821 190 0 0 25 0 1 0 542797295 322805760 72735 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78810 72735 603 41 0 78769 0
vsize: 315240
[startup+880.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75590 0 0 0 87821 190 0 0 25 0 1 0 542797295 322940928 72750 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78843 72750 603 41 0 78802 0
vsize: 315372
[startup+890.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75808 0 0 0 88820 191 0 0 25 0 1 0 542797295 323747840 72968 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79040 72968 603 41 0 78999 0
vsize: 316160
[startup+900.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75822 0 0 0 89820 191 0 0 25 0 1 0 542797295 323883008 72982 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79073 72982 603 41 0 79032 0
vsize: 316292
[startup+910.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75840 0 0 0 90821 191 0 0 25 0 1 0 542797295 323883008 73000 4294967295 134512640 134672761 3221224544 3221223640 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79073 73000 603 41 0 79032 0
vsize: 316292
[startup+920.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75852 0 0 0 91821 191 0 0 25 0 1 0 542797295 324018176 73012 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79106 73012 603 41 0 79065 0
vsize: 316424
[startup+930.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75865 0 0 0 92821 191 0 0 25 0 1 0 542797295 324018176 73025 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79106 73025 603 41 0 79065 0
vsize: 316424
[startup+940.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75875 0 0 0 93821 192 0 0 25 0 1 0 542797295 324018176 73035 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79106 73035 603 41 0 79065 0
vsize: 316424
[startup+950.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75895 0 0 0 94821 192 0 0 25 0 1 0 542797295 324153344 73055 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79139 73055 603 41 0 79098 0
vsize: 316556
[startup+960.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75907 0 0 0 95821 192 0 0 25 0 1 0 542797295 324153344 73067 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79139 73067 603 41 0 79098 0
vsize: 316556
[startup+970.071 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75920 0 0 0 96821 193 0 0 25 0 1 0 542797295 324288512 73080 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79172 73080 603 41 0 79131 0
vsize: 316688
[startup+980.071 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75938 0 0 0 97821 193 0 0 25 0 1 0 542797295 324288512 73098 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79172 73098 603 41 0 79131 0
vsize: 316688
[startup+990.071 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75949 0 0 0 98821 193 0 0 25 0 1 0 542797295 324288512 73109 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79172 73109 603 41 0 79131 0
vsize: 316688
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75965 0 0 0 99821 193 0 0 25 0 1 0 542797295 324423680 73125 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79205 73125 603 41 0 79164 0
vsize: 316820
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75975 0 0 0 100822 193 0 0 25 0 1 0 542797295 324423680 73135 4294967295 134512640 134672761 3221224544 3221223668 134566095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79205 73135 603 41 0 79164 0
vsize: 316820
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 75991 0 0 0 101822 193 0 0 25 0 1 0 542797295 324558848 73151 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79238 73151 603 41 0 79197 0
vsize: 316952
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76016 0 0 0 102821 194 0 0 25 0 1 0 542797295 324558848 73176 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79238 73176 603 41 0 79197 0
vsize: 316952
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76032 0 0 0 103822 194 0 0 25 0 1 0 542797295 324694016 73192 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79271 73192 603 41 0 79230 0
vsize: 317084
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76045 0 0 0 104822 194 0 0 25 0 1 0 542797295 324694016 73205 4294967295 134512640 134672761 3221224544 3221223680 134560579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79271 73205 603 41 0 79230 0
vsize: 317084
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76053 0 0 0 105822 194 0 0 25 0 1 0 542797295 324694016 73213 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79271 73213 603 41 0 79230 0
vsize: 317084
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76063 0 0 0 106822 194 0 0 25 0 1 0 542797295 324694016 73223 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79271 73223 603 41 0 79230 0
vsize: 317084
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76106 0 0 0 107822 194 0 0 25 0 1 0 542797295 324829184 73266 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79304 73266 603 41 0 79263 0
vsize: 317216
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76128 0 0 0 108822 194 0 0 25 0 1 0 542797295 324964352 73288 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79337 73288 603 41 0 79296 0
vsize: 317348
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76142 0 0 0 109822 194 0 0 25 0 1 0 542797295 325488640 73302 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79465 73302 603 41 0 79424 0
vsize: 317860
[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76229 0 0 0 110822 194 0 0 25 0 1 0 542797295 325758976 73389 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79531 73389 603 41 0 79490 0
vsize: 318124
[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76245 0 0 0 111822 194 0 0 25 0 1 0 542797295 325894144 73405 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79564 73405 603 41 0 79523 0
vsize: 318256
[startup+1130.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76256 0 0 0 112822 194 0 0 25 0 1 0 542797295 325894144 73416 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79564 73416 603 41 0 79523 0
vsize: 318256
[startup+1140.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76271 0 0 0 113822 195 0 0 25 0 1 0 542797295 326029312 73431 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79597 73431 603 41 0 79556 0
vsize: 318388
[startup+1150.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76297 0 0 0 114822 195 0 0 25 0 1 0 542797295 326029312 73457 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79597 73457 603 41 0 79556 0
vsize: 318388
[startup+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76313 0 0 0 115822 195 0 0 25 0 1 0 542797295 326164480 73473 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79630 73473 603 41 0 79589 0
vsize: 318520
[startup+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76331 0 0 0 116823 195 0 0 25 0 1 0 542797295 326164480 73491 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79630 73491 603 41 0 79589 0
vsize: 318520
[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76342 0 0 0 117823 195 0 0 25 0 1 0 542797295 326299648 73502 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79663 73502 603 41 0 79622 0
vsize: 318652
[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76348 0 0 0 118823 195 0 0 25 0 1 0 542797295 326299648 73508 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79663 73508 603 41 0 79622 0
vsize: 318652
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23106
Raw data (stat): 23106 (minisat+) R 23105 23176 23175 0 -1 0 76359 0 0 0 119823 195 0 0 25 0 1 0 542797295 326299648 73519 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79663 73519 603 41 0 79622 0
vsize: 318652
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 23106
Raw data (stat): 23106 (minisat+) Z 23105 23176 23175 0 -1 12 76361 0 0 0 119823 210 0 0 25 0 1 0 542797295 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.23
CPU time (s): 1200.34
CPU user time (s): 1198.23
CPU system time (s): 2.10168
CPU usage (%): 100.009
Max. virtual memory (Kb): 318652
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####