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 16038

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 06:10:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16326 boxname=wulflinc13 idbench=1256 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c56066a13a725fcc9c143db3d9f8cc06  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-sctap2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-sctap2.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-sctap2.opb
IDLAUNCH: 16326
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        778536 kB
Buffers:         33544 kB
Cached:         199792 kB
SwapCached:        176 kB
Active:          63812 kB
Inactive:       172364 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        778284 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6808 kB
Slab:            14312 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:30:20 (client local time) WITH STATUS 0 IN 1200.61 SECONDS
stats: 16326 7 1200.61 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 | 2796853  7571342 |  839055       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/815769          
c   -- var.elim.:  2000/815769          
c   -- var.elim.:  3000/815769          
c   -- var.elim.:  4000/815769          
c   -- var.elim.:  5000/815769          
c   -- var.elim.:  6000/815769          
c   -- var.elim.:  7000/815769          
c   -- var.elim.:  8000/815769          
c   -- var.elim.:  9000/815769          
c   -- var.elim.:  10000/815769          
c   -- var.elim.:  11000/815769          
c   -- var.elim.:  12000/815769          
c   -- var.elim.:  13000/815769          
c   -- var.elim.:  14000/815769          
c   -- var.elim.:  15000/815769          
c   -- var.elim.:  16000/815769          
c   -- var.elim.:  17000/815769          
c   -- var.elim.:  18000/815769          
c   -- var.elim.:  19000/815769          
c   -- var.elim.:  20000/815769          
c   -- var.elim.:  21000/815769          
c   -- var.elim.:  22000/815769          
c   -- var.elim.:  23000/815769          
c   -- var.elim.:  24000/815769          
c   -- var.elim.:  25000/815769          
c   -- var.elim.:  26000/815769          
c   -- var.elim.:  27000/815769          
c   -- var.elim.:  28000/815769          
c   -- var.elim.:  29000/815769          
c   -- var.elim.:  30000/815769          
c   -- var.elim.:  31000/815769          
c   -- var.elim.:  32000/815769          
c   -- var.elim.:  33000/815769          
c   -- var.elim.:  34000/815769          
c   -- var.elim.:  35000/815769          
c   -- var.elim.:  36000/815769          
c   -- var.elim.:  37000/815769          
c   -- var.elim.:  38000/815769          
c   -- var.elim.:  39000/815769          
c   -- var.elim.:  40000/815769          
c   -- var.elim.:  41000/815769          
c   -- var.elim.:  42000/815769          
c   -- var.elim.:  43000/815769          
c   -- var.elim.:  44000/815769          
c   -- var.elim.:  45000/815769          
c   -- var.elim.:  46000/815769          
c   -- var.elim.:  47000/815769          
c   -- var.elim.:  48000/815769          
c   -- var.elim.:  49000/815769          
c   -- var.elim.:  50000/815769          
c   -- var.elim.:  51000/815769          
c   -- var.elim.:  52000/815769          
c   -- var.elim.:  53000/815769          
c   -- var.elim.:  54000/815769          
c   -- var.elim.:  55000/815769          
c   -- var.elim.:  56000/815769          
c   -- var.elim.:  57000/815769          
c   -- var.elim.:  58000/815769          
c   -- var.elim.:  59000/815769          
c   -- var.elim.:  60000/815769          
c   -- var.elim.:  61000/815769          
c   -- var.elim.:  62000/815769          
c   -- var.elim.:  63000/815769          
c   -- var.elim.:  64000/815769          
c   -- var.elim.:  65000/815769          
c   -- var.elim.:  66000/815769          
c   -- var.elim.:  67000/815769          
c   -- var.elim.:  68000/815769          
c   -- var.elim.:  69000/815769          
c   -- var.elim.:  70000/815769          
c   -- var.elim.:  71000/815769          
c   -- var.elim.:  72000/815769          
c   -- var.elim.:  73000/815769          
c   -- var.elim.:  74000/815769          
c   -- var.elim.:  75000/815769          
c   -- var.elim.:  76000/815769          
c   -- var.elim.:  77000/815769          
c   -- var.elim.:  78000/815769          
c   -- var.elim.:  79000/815769          
c   -- var.elim.:  80000/815769          
c   -- var.elim.:  81000/815769          
c   -- var.elim.:  82000/815769          
c   -- var.elim.:  83000/815769          
c   -- var.elim.:  84000/815769          
c   -- var.elim.:  85000/815769          
c   -- var.elim.:  86000/815769          
c   -- var.elim.:  87000/815769          
c   -- var.elim.:  88000/815769          
c   -- var.elim.:  89000/815769          
c   -- var.elim.:  90000/815769          
c   -- var.elim.:  91000/815769          
c   -- var.elim.:  92000/815769          
c   -- var.elim.:  93000/815769          
c   -- var.elim.:  94000/815769          
c   -- var.elim.:  95000/815769          
c   -- var.elim.:  96000/815769          
c   -- var.elim.:  97000/815769          
c   -- var.elim.:  98000/815769          
c   -- var.elim.:  99000/815769          
c   -- var.elim.:  100000/815769          
c   -- var.elim.:  101000/815769          
c   -- var.elim.:  102000/815769          
c   -- var.elim.:  103000/815769          
c   -- var.elim.:  104000/815769          
c   -- var.elim.:  105000/815769          
c   -- var.elim.:  106000/815769          
c   -- var.elim.:  107000/815769          
c   -- var.elim.:  108000/815769          
c   -- var.elim.:  109000/815769          
c   -- var.elim.:  110000/815769          
c   -- var.elim.:  111000/815769          
c   -- var.elim.:  112000/815769          
c   -- var.elim.:  113000/815769          
c   -- var.elim.:  114000/815769          
c   -- var.elim.:  115000/815769          
c   -- var.elim.:  116000/815769          
c   -- var.elim.:  117000/815769          
c   -- var.elim.:  118000/815769          
c   -- var.elim.:  119000/815769          
c   -- var.elim.:  120000/815769          
c   -- var.elim.:  121000/815769          
c   -- var.elim.:  122000/815769          
c   -- var.elim.:  123000/815769          
c   -- var.elim.:  124000/815769          
c   -- var.elim.:  125000/815769          
c   -- var.elim.:  126000/815769          
c   -- var.elim.:  127000/815769          
c   -- var.elim.:  128000/815769          
c   -- var.elim.:  129000/815769          
c   -- var.elim.:  130000/815769          
c   -- var.elim.:  131000/815769          
c   -- var.elim.:  132000/815769          
c   -- var.elim.:  133000/815769          
c   -- var.elim.:  134000/815769          
c   -- var.elim.:  135000/815769          
c   -- var.elim.:  136000/815769          
c   -- var.elim.:  137000/815769          
c   -- var.elim.:  138000/815769          
c   -- var.elim.:  139000/815769          
c   -- var.elim.:  140000/815769          
c   -- var.elim.:  141000/815769          
c   -- var.elim.:  142000/815769          
c   -- var.elim.:  143000/815769          
c   -- var.elim.:  144000/815769          
c   -- var.elim.:  145000/815769          
c   -- var.elim.:  146000/815769          
c   -- var.elim.:  147000/815769          
c   -- var.elim.:  148000/815769          
c   -- var.elim.:  149000/815769          
c   -- var.elim.:  150000/815769          
c   -- var.elim.:  151000/815769          
c   -- var.elim.:  152000/815769          
c   -- var.elim.:  153000/815769          
c   -- var.elim.:  154000/815769          
c   -- var.elim.:  155000/815769          
c   -- var.elim.:  156000/815769          
c   -- var.elim.:  157000/815769          
c   -- var.elim.:  158000/815769          
c   -- var.elim.:  159000/815769          
c   -- var.elim.:  160000/815769          
c   -- var.elim.:  161000/815769          
c   -- var.elim.:  162000/815769          
c   -- var.elim.:  163000/815769          
c   -- var.elim.:  164000/815769          
c   -- var.elim.:  165000/815769          
c   -- var.elim.:  166000/815769          
c   -- var.elim.:  167000/815769          
c   -- var.elim.:  168000/815769          
c   -- var.elim.:  169000/815769          
c   -- var.elim.:  170000/815769          
c   -- var.elim.:  171000/815769          
c   -- var.elim.:  172000/815769          
c   -- var.elim.:  173000/815769          
c   -- var.elim.:  174000/815769          
c   -- var.elim.:  175000/815769          
c   -- var.elim.:  176000/815769          
c   -- var.elim.:  177000/815769          
c   -- var.elim.:  178000/815769          
c   -- var.elim.:  179000/815769          
c   -- var.elim.:  180000/815769          
c   -- var.elim.:  181000/815769          
c   -- var.elim.:  182000/815769          
c   -- var.elim.:  183000/815769          
c   -- var.elim.:  184000/815769          
c   -- var.elim.:  185000/815769          
c   -- var.elim.:  186000/815769          
c   -- var.elim.:  187000/815769          
c   -- var.elim.:  188000/815769          
c   -- var.elim.:  189000/815769          
c   -- var.elim.:  190000/815769          
c   -- var.elim.:  191000/815769          
c   -- var.elim.:  192000/815769          
c   -- var.elim.:  193000/815769          
c   -- var.elim.:  194000/815769          
c   -- var.elim.:  195000/815769          
c   -- var.elim.:  196000/815769          
c   -- var.elim.:  197000/815769          
c   -- var.elim.:  198000/815769          
c   -- var.elim.:  199000/815769          
c   -- var.elim.:  200000/815769          
c   -- var.elim.:  201000/815769          
c   -- var.elim.:  202000/815769          
c   -- var.elim.:  203000/815769          
c   -- var.elim.:  204000/815769          
c   -- var.elim.:  205000/815769          
c   -- var.elim.:  206000/815769          
c   -- var.elim.:  207000/815769          
c   -- var.elim.:  208000/815769          
c   -- var.elim.:  209000/815769          
c   -- var.elim.:  210000/815769          
c   -- var.elim.:  211000/815769          
c   -- var.elim.:  212000/815769          
c   -- var.elim.:  213000/815769          
c   -- var.elim.:  214000/815769          
c   -- var.elim.:  215000/815769          
c   -- var.elim.:  216000/815769          
c   -- var.elim.:  217000/815769          
c   -- var.elim.:  218000/815769          
c   -- var.elim.:  219000/815769          
c   -- var.elim.:  220000/815769          
c   -- var.elim.:  221000/815769          
c   -- var.elim.:  222000/815769          
c   -- var.elim.:  223000/815769          
c   -- var.elim.:  224000/815769          
c   -- var.elim.:  225000/815769          
c   -- var.elim.:  226000/815769          
c   -- var.elim.:  227000/815769          
c   -- var.elim.:  228000/815769          
c   -- var.elim.:  229000/815769          
c   -- var.elim.:  230000/815769          
c   -- var.elim.:  231000/815769          
c   -- var.elim.:  232000/815769          
c   -- var.elim.:  233000/815769          
c   -- var.elim.:  234000/815769          
c   -- var.elim.:  235000/815769          
c   -- var.elim.:  236000/815769          
c   -- var.elim.:  237000/815769          
c   -- var.elim.:  238000/815769          
c   -- var.elim.:  239000/815769          
c   -- var.elim.:  240000/815769          
c   -- var.elim.:  241000/815769          
c   -- var.elim.:  242000/815769          
c   -- var.elim.:  243000/815769          
c   -- var.elim.:  244000/815769          
c   -- var.elim.:  245000/815769          
c   -- var.elim.:  246000/815769          
c   -- var.elim.:  247000/815769          
c   -- var.elim.:  248000/815769          
c   -- var.elim.:  249000/815769          
c   -- var.elim.:  250000/815769          
c   -- var.elim.:  251000/815769          
c   -- var.elim.:  252000/815769          
c   -- var.elim.:  253000/815769          
c   -- var.elim.:  254000/815769          
c   -- var.elim.:  255000/815769          
c   -- var.elim.:  256000/815769          
c   -- var.elim.:  257000/815769          
c   -- var.elim.:  258000/815769          
c   -- var.elim.:  259000/815769          
c   -- var.elim.:  260000/815769          
c   -- var.elim.:  261000/815769          
c   -- var.elim.:  262000/815769          
c   -- var.elim.:  263000/815769          
c   -- var.elim.:  264000/815769          
c   -- var.elim.:  265000/815769          
c   -- var.elim.:  266000/815769          
c   -- var.elim.:  267000/815769          
c   -- var.elim.:  268000/815769          
c   -- var.elim.:  269000/815769          
c   -- var.elim.:  270000/815769          
c   -- var.elim.:  271000/815769          
c   -- var.elim.:  272000/815769          
c   -- var.elim.:  273000/815769          
c   -- var.elim.:  274000/815769          
c   -- var.elim.:  275000/815769          
c   -- var.elim.:  276000/815769          
c   -- var.elim.:  277000/815769          
c   -- var.elim.:  278000/815769          
c   -- var.elim.:  279000/815769          
c   -- var.elim.:  280000/815769          
c   -- var.elim.:  281000/815769          
c   -- var.elim.:  282000/815769          
c   -- var.elim.:  283000/815769          
c   -- var.elim.:  284000/815769          
c   -- var.elim.:  285000/815769          
c   -- var.elim.:  286000/815769          
c   -- var.elim.:  287000/815769          
c   -- var.elim.:  288000/815769          
c   -- var.elim.:  289000/815769          
c   -- var.elim.:  290000/815769          
c   -- var.elim.:  291000/815769          
c   -- var.elim.:  292000/815769          
c   -- var.elim.:  293000/815769          
c   -- var.elim.:  294000/815769          
c   -- var.elim.:  295000/815769          
c   -- var.elim.:  296000/815769          
c   -- var.elim.:  297000/815769          
c   -- var.elim.:  298000/815769          
c   -- var.elim.:  299000/815769          
c   -- var.elim.:  300000/815769          
c   -- var.elim.:  301000/815769          
c   -- var.elim.:  302000/815769          
c   -- var.elim.:  303000/815769          
c   -- var.elim.:  304000/815769          
c   -- var.elim.:  305000/815769          
c   -- var.elim.:  306000/815769          
c   -- var.elim.:  307000/815769          
c   -- var.elim.:  308000/815769          
c   -- var.elim.:  309000/815769          
c   -- var.elim.:  310000/815769          
c   -- var.elim.:  311000/815769          
c   -- var.elim.:  312000/815769          
c   -- var.elim.:  313000/815769          
c   -- var.elim.:  314000/815769          
c   -- var.elim.:  315000/815769          
c   -- var.elim.:  316000/815769          
c   -- var.elim.:  317000/815769          
c   -- var.elim.:  318000/815769          
c   -- var.elim.:  319000/815769          
c   -- var.elim.:  320000/815769          
c   -- var.elim.:  321000/815769          
c   -- var.elim.:  322000/815769          
c   -- var.elim.:  323000/815769          
c   -- var.elim.:  324000/815769          
c   -- var.elim.:  325000/815769          
c   -- var.elim.:  326000/815769          
c   -- var.elim.:  327000/815769          
c   -- var.elim.:  328000/815769          
c   -- var.elim.:  329000/815769          
c   -- var.elim.:  330000/815769          
c   -- var.elim.:  331000/815769          
c   -- var.elim.:  332000/815769          
c   -- var.elim.:  333000/815769          
c   -- var.elim.:  334000/815769          
c   -- var.elim.:  335000/815769          
c   -- var.elim.:  336000/815769          
c   -- var.elim.:  337000/815769          
c   -- var.elim.:  338000/815769          
c   -- var.elim.:  339000/815769          
c   -- var.elim.:  340000/815769          
c   -- var.elim.:  341000/815769          
c   -- var.elim.:  342000/815769          
c   -- var.elim.:  343000/815769          
c   -- var.elim.:  344000/815769          
c   -- var.elim.:  345000/815769          
c   -- var.elim.:  346000/815769          
c   -- var.elim.:  347000/815769          
c   -- var.elim.:  348000/815769          
c   -- var.elim.:  349000/815769          
c   -- var.elim.:  350000/815769          
c   -- var.elim.:  351000/815769          
c   -- var.elim.:  352000/815769          
c   -- var.elim.:  353000/815769          
c   -- var.elim.:  354000/815769          
c   -- var.elim.:  355000/815769          
c   -- var.elim.:  356000/815769          
c   -- var.elim.:  357000/815769          
c   -- var.elim.:  358000/815769          
c   -- var.elim.:  359000/815769          
c   -- var.elim.:  360000/815769          
c   -- var.elim.:  361000/815769          
c   -- var.elim.:  362000/815769          
c   -- var.elim.:  363000/815769          
c   -- var.elim.:  364000/815769          
c   -- var.elim.:  365000/815769          
c   -- var.elim.:  366000/815769          
c   -- var.elim.:  367000/815769          
c   -- var.elim.:  368000/815769          
c   -- var.elim.:  369000/815769          
c   -- var.elim.:  370000/815769          
c   -- var.elim.:  371000/815769          
c   -- var.elim.:  372000/815769          
c   -- var.elim.:  373000/815769          
c   -- var.elim.:  374000/815769          
c   -- var.elim.:  375000/815769          
c   -- var.elim.:  376000/815769          
c   -- var.elim.:  377000/815769          
c   -- var.elim.:  378000/815769          
c   -- var.elim.:  379000/815769          
c   -- var.elim.:  380000/815769          
c   -- var.elim.:  381000/815769          
c   -- var.elim.:  382000/815769          
c   -- var.elim.:  383000/815769          
c   -- var.elim.:  384000/815769          
c   -- var.elim.:  385000/815769          
c   -- var.elim.:  386000/815769          
c   -- var.elim.:  387000/815769          
c   -- var.elim.:  388000/815769          
c   -- var.elim.:  389000/815769          
c   -- var.elim.:  390000/815769          
c   -- var.elim.:  391000/815769          
c   -- var.elim.:  392000/815769          
c   -- var.elim.:  393000/815769          
c   -- var.elim.:  394000/815769          
c   -- var.elim.:  395000/815769          
c   -- var.elim.:  396000/815769          
c   -- var.elim.:  397000/815769          
c   -- var.elim.:  398000/815769          
c   -- var.elim.:  399000/815769          
c   -- var.elim.:  400000/815769          
c   -- var.elim.:  401000/815769          
c   -- var.elim.:  402000/815769          
c   -- var.elim.:  403000/815769          
c   -- var.elim.:  404000/815769          
c   -- var.elim.:  405000/815769          
c   -- var.elim.:  406000/815769          
c   -- var.elim.:  407000/815769          
c   -- var.elim.:  408000/815769          
c   -- var.elim.:  409000/815769          
c   -- var.elim.:  410000/815769          
c   -- var.elim.:  411000/815769          
c   -- var.elim.:  412000/815769          
c   -- var.elim.:  413000/815769          
c   -- var.elim.:  414000/815769          
c   -- var.elim.:  415000/815769          
c   -- var.elim.:  416000/815769          
c   -- var.elim.:  417000/815769          
c   -- var.elim.:  418000/815769          
c   -- var.elim.:  419000/815769          
c   -- var.elim.:  420000/815769          
c   -- var.elim.:  421000/815769          
c   -- var.elim.:  422000/815769          
c   -- var.elim.:  423000/815769          
c   -- var.elim.:  424000/815769          
c   -- var.elim.:  425000/815769          
c   -- var.elim.:  426000/815769          
c   -- var.elim.:  427000/815769          
c   -- var.elim.:  428000/815769          
c   -- var.elim.:  429000/815769          
c   -- var.elim.:  430000/815769          
c   -- var.elim.:  431000/815769          
c   -- var.elim.:  432000/815769          
c   -- var.elim.:  433000/815769          
c   -- var.elim.:  434000/815769          
c   -- var.elim.:  435000/815769          
c   -- var.elim.:  436000/815769          
c   -- var.elim.:  437000/815769          
c   -- var.elim.:  438000/815769          
c   -- var.elim.:  439000/815769          
c   -- var.elim.:  440000/815769          
c   -- var.elim.:  441000/815769          
c   -- var.elim.:  442000/815769          
c   -- var.elim.:  443000/815769          
c   -- var.elim.:  444000/815769          
c   -- var.elim.:  445000/815769          
c   -- var.elim.:  446000/815769          
c   -- var.elim.:  447000/815769          
c   -- var.elim.:  448000/815769          
c   -- var.elim.:  449000/815769          
c   -- var.elim.:  450000/815769          
c   -- var.elim.:  451000/815769          
c   -- var.elim.:  452000/815769          
c   -- var.elim.:  453000/815769          
c   -- var.elim.:  454000/815769          
c   -- var.elim.:  455000/815769          
c   -- var.elim.:  456000/815769          
c   -- var.elim.:  457000/815769          
c   -- var.elim.:  458000/815769          
c   -- var.elim.:  459000/815769          
c   -- var.elim.:  460000/815769          
c   -- var.elim.:  461000/815769          
c   -- var.elim.:  462000/815769          
c   -- var.elim.:  463000/815769          
c   -- var.elim.:  464000/815769          
c   -- var.elim.:  465000/815769          
c   -- var.elim.:  466000/815769          
c   -- var.elim.:  467000/815769          
c   -- var.elim.:  468000/815769          
c   -- var.elim.:  469000/815769          
c   -- var.elim.:  470000/815769          
c   -- var.elim.:  471000/815769          
c   -- var.elim.:  472000/815769          
c   -- var.elim.:  473000/815769          
c   -- var.elim.:  474000/815769          
c   -- var.elim.:  475000/815769          
c   -- var.elim.:  476000/815769          
c   -- var.elim.:  477000/815769          
c   -- var.elim.:  478000/815769          
c   -- var.elim.:  479000/815769          
c   -- var.elim.:  480000/815769          
c   -- var.elim.:  481000/815769          
c   -- var.elim.:  482000/815769          
c   -- var.elim.:  483000/815769          
c   -- var.elim.:  484000/815769          
c   -- var.elim.:  485000/815769          
c   -- var.elim.:  486000/815769          
c   -- var.elim.:  487000/815769          
c   -- var.elim.:  488000/815769          
c   -- var.elim.:  489000/815769          
c   -- var.elim.:  490000/815769          
c   -- var.elim.:  491000/815769          
c   -- var.elim.:  492000/815769          
c   -- var.elim.:  493000/815769          
c   -- var.elim.:  494000/815769          
c   -- var.elim.:  495000/815769          
c   -- var.elim.:  496000/815769          
c   -- var.elim.:  497000/815769          
c   -- var.elim.:  498000/815769          
c   -- var.elim.:  499000/815769          
c   -- var.elim.:  500000/815769          
c   -- var.elim.:  501000/815769          
c   -- var.elim.:  502000/815769          
c   -- var.elim.:  503000/815769          
c   -- var.elim.:  504000/815769          
c   -- var.elim.:  505000/815769          
c   -- var.elim.:  506000/815769          
c   -- var.elim.:  507000/815769          
c   -- var.elim.:  508000/815769          
c   -- var.elim.:  509000/815769          
c   -- var.elim.:  510000/815769          
c   -- var.elim.:  511000/815769          
c   -- var.elim.:  512000/815769          
c   -- var.elim.:  513000/815769          
c   -- var.elim.:  514000/815769          
c   -- var.elim.:  515000/815769          
c   -- var.elim.:  516000/815769          
c   -- var.elim.:  517000/815769          
c   -- var.elim.:  518000/815769          
c   -- var.elim.:  519000/815769          
c   -- var.elim.:  520000/815769          
c   -- var.elim.:  521000/815769          
c   -- var.elim.:  522000/815769          
c   -- var.elim.:  523000/815769          
c   -- var.elim.:  524000/815769          
c   -- var.elim.:  525000/815769          
c   -- var.elim.:  526000/815769          
c   -- var.elim.:  527000/815769          
c   -- var.elim.:  528000/815769          
c   -- var.elim.:  529000/815769          
c   -- var.elim.:  530000/815769          
c   -- var.elim.:  531000/815769          
c   -- var.elim.:  532000/815769          
c   -- var.elim.:  533000/815769          
c   -- var.elim.:  534000/815769          
c   -- var.elim.:  535000/815769          
c   -- var.elim.:  536000/815769          
c   -- var.elim.:  537000/815769          
c   -- var.elim.:  538000/815769          
c   -- var.elim.:  539000/815769          
c   -- var.elim.:  540000/815769          
c   -- var.elim.:  541000/815769          
c   -- var.elim.:  542000/815769          
c   -- var.elim.:  543000/815769          
c   -- var.elim.:  544000/815769          
c   -- var.elim.:  545000/815769          
c   -- var.elim.:  546000/815769          
c   -- var.elim.:  547000/815769          
c   -- var.elim.:  548000/815769          
c   -- var.elim.:  549000/815769          
c   -- var.elim.:  550000/815769          
c   -- var.elim.:  551000/815769          
c   -- var.elim.:  552000/815769          
c   -- var.elim.:  553000/815769          
c   -- var.elim.:  554000/815769          
c   -- var.elim.:  555000/815769          
c   -- var.elim.:  556000/815769          
c   -- var.elim.:  557000/815769          
c   -- var.elim.:  558000/815769          
c   -- var.elim.:  559000/815769          
c   -- var.elim.:  560000/815769          
c   -- var.elim.:  561000/815769          
c   -- var.elim.:  562000/815769          
c   -- var.elim.:  563000/815769          
c   -- var.elim.:  564000/815769          
c   -- var.elim.:  565000/815769          
c   -- var.elim.:  566000/815769          
c   -- var.elim.:  567000/815769          
c   -- var.elim.:  568000/815769          
c   -- var.elim.:  569000/815769          
c   -- var.elim.:  570000/815769          
c   -- var.elim.:  571000/815769          
c   -- var.elim.:  572000/815769          
c   -- var.elim.:  573000/815769          
c   -- var.elim.:  574000/815769          
c   -- var.elim.:  575000/815769          
c   -- var.elim.:  576000/815769          
c   -- var.elim.:  577000/815769          
c   -- var.elim.:  578000/815769          
c   -- var.elim.:  579000/815769          
c   -- var.elim.:  580000/815769          
c   -- var.elim.:  581000/815769          
c   -- var.elim.:  582000/815769          
c   -- var.elim.:  583000/815769          
c   -- var.elim.:  584000/815769          
c   -- var.elim.:  585000/815769          
c   -- var.elim.:  586000/815769          
c   -- var.elim.:  587000/815769          
c   -- var.elim.:  588000/815769          
c   -- var.elim.:  589000/815769          
c   -- var.elim.:  590000/815769          
c   -- var.elim.:  591000/815769          
c   -- var.elim.:  592000/815769          
c   -- var.elim.:  593000/815769          
c   -- var.elim.:  594000/815769          
c   -- var.elim.:  595000/815769          
c   -- var.elim.:  596000/815769          
c   -- var.elim.:  597000/815769          
c   -- var.elim.:  598000/815769          
c   -- var.elim.:  599000/815769          
c   -- var.elim.:  600000/815769          
c   -- var.elim.:  601000/815769          
c   -- var.elim.:  602000/815769          
c   -- var.elim.:  603000/815769          
c   -- var.elim.:  604000/815769          
c   -- var.elim.:  605000/815769          
c   -- var.elim.:  606000/815769          
c   -- var.elim.:  607000/815769          
c   -- var.elim.:  608000/815769          
c   -- var.elim.:  609000/815769          
c   -- var.elim.:  610000/815769          
c   -- var.elim.:  611000/815769          
c   -- var.elim.:  612000/815769          
c   -- var.elim.:  613000/815769          
c   -- var.elim.:  614000/815769          
c   -- var.elim.:  615000/815769          
c   -- var.elim.:  616000/815769          
c   -- var.elim.:  617000/815769          
c   -- var.elim.:  618000/815769          
c   -- var.elim.:  619000/815769          
c   -- var.elim.:  620000/815769          
c   -- var.elim.:  621000/815769          
c   -- var.elim.:  622000/815769          
c   -- var.elim.:  623000/815769          
c   -- var.elim.:  624000/815769          
c   -- var.elim.:  625000/815769          
c   -- var.elim.:  626000/815769          
c   -- var.elim.:  627000/815769          
c   -- var.elim.:  628000/815769          
c   -- var.elim.:  629000/815769          
c   -- var.elim.:  630000/815769          
c   -- var.elim.:  631000/815769          
c   -- var.elim.:  632000/815769          
c   -- var.elim.:  633000/815769          
c   -- var.elim.:  634000/815769          
c   -- var.elim.:  635000/815769          
c   -- var.elim.:  636000/815769          
c   -- var.elim.:  637000/815769          
c   -- var.elim.:  638000/815769          
c   -- var.elim.:  639000/815769          
c   -- var.elim.:  640000/815769          
c   -- var.elim.:  641000/815769          
c   -- var.elim.:  642000/815769          
c   -- var.elim.:  643000/815769          
c   -- var.elim.:  644000/815769          
c   -- var.elim.:  645000/815769          
c   -- var.elim.:  646000/815769          
c   -- var.elim.:  647000/815769          
c   -- var.elim.:  648000/815769          
c   -- var.elim.:  649000/815769          
c   -- var.elim.:  650000/815769          
c   -- var.elim.:  651000/815769          
c   -- var.elim.:  652000/815769          
c   -- var.elim.:  653000/815769          
c   -- var.elim.:  654000/815769          
c   -- var.elim.:  655000/815769          
c   -- var.elim.:  656000/815769          
c   -- var.elim.:  657000/815769          
c   -- var.elim.:  658000/815769          
c   -- var.elim.:  659000/815769          
c   -- var.elim.:  660000/815769          
c   -- var.elim.:  661000/815769          
c   -- var.elim.:  662000/815769          
c   -- var.elim.:  663000/815769          
c   -- var.elim.:  664000/815769          
c   -- var.elim.:  665000/815769          
c   -- var.elim.:  666000/815769          
c   -- var.elim.:  667000/815769          
c   -- var.elim.:  668000/815769          
c   -- var.elim.:  669000/815769          
c   -- var.elim.:  670000/815769          
c   -- var.elim.:  671000/815769          
c   -- var.elim.:  672000/815769          
c   -- var.elim.:  673000/815769          
c   -- var.elim.:  674000/815769          
c   -- var.elim.:  675000/815769          
c   -- var.elim.:  676000/815769          
c   -- var.elim.:  677000/815769          
c   -- var.elim.:  678000/815769          
c   -- var.elim.:  679000/815769          
c   -- var.elim.:  680000/815769          
c   -- var.elim.:  681000/815769          
c   -- var.elim.:  682000/815769          
c   -- var.elim.:  683000/815769          
c   -- var.elim.:  684000/815769          
c   -- var.elim.:  685000/815769          
c   -- var.elim.:  686000/815769          
c   -- var.elim.:  687000/815769          
c   -- var.elim.:  688000/815769          
c   -- var.elim.:  689000/815769          
c   -- var.elim.:  690000/815769          
c   -- var.elim.:  691000/815769          
c   -- var.elim.:  692000/815769          
c   -- var.elim.:  693000/815769          
c   -- var.elim.:  694000/815769          
c   -- var.elim.:  695000/815769          
c   -- var.elim.:  696000/815769          
c   -- var.elim.:  697000/815769          
c   -- var.elim.:  698000/815769          
c   -- var.elim.:  699000/815769          
c   -- var.elim.:  700000/815769          
c   -- var.elim.:  701000/815769          
c   -- var.elim.:  702000/815769          
c   -- var.elim.:  703000/815769          
c   -- var.elim.:  704000/815769          
c   -- var.elim.:  705000/815769          
c   -- var.elim.:  706000/815769          
c   -- var.elim.:  707000/815769          
c   -- var.elim.:  708000/815769          
c   -- var.elim.:  709000/815769          
c   -- var.elim.:  710000/815769          
c   -- var.elim.:  711000/815769          
c   -- var.elim.:  712000/815769          
c   -- var.elim.:  713000/815769          
c   -- var.elim.:  714000/815769          
c   -- var.elim.:  715000/815769          
c   -- var.elim.:  716000/815769          
c   -- var.elim.:  717000/815769          
c   -- var.elim.:  718000/815769          
c   -- var.elim.:  719000/815769          
c   -- var.elim.:  720000/815769          
c   -- var.elim.:  721000/815769          
c   -- var.elim.:  722000/815769          
c   -- var.elim.:  723000/815769          
c   -- var.elim.:  724000/815769          
c   -- var.elim.:  725000/815769          
c   -- var.elim.:  726000/815769          
c   -- var.elim.:  727000/815769          
c   -- var.elim.:  728000/815769          
c   -- var.elim.:  729000/815769          
c   -- var.elim.:  730000/815769          
c   -- var.elim.:  731000/815769          
c   -- var.elim.:  732000/815769          
c   -- var.elim.:  733000/815769          
c   -- var.elim.:  734000/815769          
c   -- var.elim.:  735000/815769          
c   -- var.elim.:  736000/815769          
c   -- var.elim.:  737000/815769          
c   -- var.elim.:  738000/815769          
c   -- var.elim.:  739000/815769          
c   -- var.elim.:  740000/815769          
c   -- var.elim.:  741000/815769          
c   -- var.elim.:  742000/815769          
c   -- var.elim.:  743000/815769          
c   -- var.elim.:  744000/815769          
c   -- var.elim.:  745000/815769          
c   -- var.elim.:  746000/815769          
c   -- var.elim.:  747000/815769          
c   -- var.elim.:  748000/815769          
c   -- var.elim.:  749000/815769          
c   -- var.elim.:  750000/815769          
c   -- var.elim.:  751000/815769          
c   -- var.elim.:  752000/815769          
c   -- var.elim.:  753000/815769          
c   -- var.elim.:  754000/815769          
c   -- var.elim.:  755000/815769          
c   -- var.elim.:  756000/815769          
c   -- var.elim.:  757000/815769          
c   -- var.elim.:  758000/815769          
c   -- var.elim.:  759000/815769          
c   -- var.elim.:  760000/815769          
c   -- var.elim.:  761000/815769          
c   -- var.elim.:  762000/815769          
c   -- var.elim.:  763000/815769          
c   -- var.elim.:  764000/815769          
c   -- var.elim.:  765000/815769          
c   -- var.elim.:  766000/815769          
c   -- var.elim.:  767000/815769          
c   -- var.elim.:  768000/815769          
c   -- var.elim.:  769000/815769          
c   -- var.elim.:  770000/815769          
c   -- var.elim.:  771000/815769          
c   -- var.elim.:  772000/815769          
c   -- var.elim.:  773000/815769          
c   -- var.elim.:  774000/815769          
c   -- var.elim.:  775000/815769          
c   -- var.elim.:  776000/815769          
c   -- var.elim.:  777000/815769          
c   -- var.elim.:  778000/815769          
c   -- var.elim.:  779000/815769          
c   -- var.elim.:  780000/815769          
c   -- var.elim.:  781000/815769          
c   -- var.elim.:  782000/815769          
c   -- var.elim.:  783000/815769          
c   -- var.elim.:  784000/815769          
c   -- var.elim.:  785000/815769          
c   -- var.elim.:  786000/815769          
c   -- var.elim.:  787000/815769          
c   -- var.elim.:  788000/815769          
c   -- var.elim.:  789000/815769          
c   -- var.elim.:  790000/815769          
c   -- var.elim.:  791000/815769          
c   -- var.elim.:  792000/815769          
c   -- var.elim.:  793000/815769          
c   -- var.elim.:  794000/815769          
c   -- var.elim.:  795000/815769          
c   -- var.elim.:  796000/815769          
c   -- var.elim.:  797000/815769          
c   -- var.elim.:  798000/815769          
c   -- var.elim.:  799000/815769          
c   -- var.elim.:  800000/815769          
c   -- var.elim.:  801000/815769          
c   -- var.elim.:  802000/815769          
c   -- var.elim.:  803000/815769          
c   -- var.elim.:  804000/815769          
c   -- var.elim.:  805000/815769          
c   -- var.elim.:  806000/815769          
c   -- var.elim.:  807000/815769          
c   -- var.elim.:  808000/815769          
c   -- var.elim.:  809000/815769          
c   -- var.elim.:  810000/815769          
c   -- var.elim.:  811000/815769          
c   -- var.elim.:  812000/815769          
c   -- var.elim.:  813000/815769          
c   -- var.elim.:  814000/815769          
c   -- var.elim.:  815000/815769          
c   -- var.elim.:  815769/815769          
c   -- var.elim.:  1000/381868          
c   -- var.elim.:  2000/381868          
c   -- var.elim.:  3000/381868          
c   -- var.elim.:  4000/381868          
c   -- var.elim.:  5000/381868          
c   -- var.elim.:  6000/381868          
c   -- var.elim.:  7000/381868          
c   -- var.elim.:  8000/381868          
c   -- var.elim.:  9000/381868          
c   -- var.elim.:  10000/381868          
c   -- var.elim.:  11000/381868          
c   -- var.elim.:  12000/381868          
c   -- var.elim.:  13000/381868          
c   -- var.elim.:  14000/381868          
c   -- var.elim.:  15000/381868          
c   -- var.elim.:  16000/381868          
c   -- var.elim.:  17000/381868          
c   -- var.elim.:  18000/381868          
c   -- var.elim.:  19000/381868          
c   -- var.elim.:  20000/381868          
c   -- var.elim.:  21000/381868          
c   -- var.elim.:  22000/381868          
c   -- var.elim.:  23000/381868          
c   -- var.elim.:  24000/381868          
c   -- var.elim.:  25000/381868          
c   -- var.elim.:  26000/381868          
c   -- var.elim.:  27000/381868          
c   -- var.elim.:  28000/381868          
c   -- var.elim.:  29000/381868          
c   -- var.elim.:  30000/381868          
c   -- var.elim.:  31000/381868          
c   -- var.elim.:  32000/381868          
c   -- var.elim.:  33000/381868          
c   -- var.elim.:  34000/381868          
c   -- var.elim.:  35000/381868          
c   -- var.elim.:  36000/381868          
c   -- var.elim.:  37000/381868          
c   -- var.elim.:  38000/381868          
c   -- var.elim.:  39000/381868          
c   -- var.elim.:  40000/381868          
c   -- var.elim.:  41000/381868          
c   -- var.elim.:  42000/381868          
c   -- var.elim.:  43000/381868          
c   -- var.elim.:  44000/381868          
c   -- var.elim.:  45000/381868          
c   -- var.elim.:  46000/381868          
c   -- var.elim.:  47000/381868          
c   -- var.elim.:  48000/381868          
c   -- var.elim.:  49000/381868          
c   -- var.elim.:  50000/381868          
c   -- var.elim.:  51000/381868          
c   -- var.elim.:  52000/381868          
c   -- var.elim.:  53000/381868          
c   -- var.elim.:  54000/381868          
c   -- var.elim.:  55000/381868          
c   -- var.elim.:  56000/381868          
c   -- var.elim.:  57000/381868          
c   -- var.elim.:  58000/381868          
c   -- var.elim.:  59000/381868          
c   -- var.elim.:  60000/381868          
c   -- var.elim.:  61000/381868          
c   -- var.elim.:  62000/381868          
c   -- var.elim.:  63000/381868          
c   -- var.elim.:  64000/381868          
c   -- var.elim.:  65000/381868          
c   -- var.elim.:  66000/381868          
c   -- var.elim.:  67000/381868          
c   -- var.elim.:  68000/381868          
c   -- var.elim.:  69000/381868          
c   -- var.elim.:  70000/381868          
c   -- var.elim.:  71000/381868          
c   -- var.elim.:  72000/381868          
c   -- var.elim.:  73000/381868          
c   -- var.elim.:  74000/381868          
c   -- var.elim.:  75000/381868          
c   -- var.elim.:  76000/381868          
c   -- var.elim.:  77000/381868          
c   -- var.elim.:  78000/381868          
c   -- var.elim.:  79000/381868          
c   -- var.elim.:  80000/381868          
c   -- var.elim.:  81000/381868          
c   -- var.elim.:  82000/381868          
c   -- var.elim.:  83000/381868          
c   -- var.elim.:  84000/381868          
c   -- var.elim.:  85000/381868          
c   -- var.elim.:  86000/381868          
c   -- var.elim.:  87000/381868          
c   -- var.elim.:  88000/381868          
c   -- var.elim.:  89000/381868          
c   -- var.elim.:  90000/381868          
c   -- var.elim.:  91000/381868          
c   -- var.elim.:  92000/381868          
c   -- var.elim.:  93000/381868          
c   -- var.elim.:  94000/381868          
c   -- var.elim.:  95000/381868          
c   -- var.elim.:  96000/381868          
c   -- var.elim.:  97000/381868          
c   -- var.elim.:  98000/381868          
c   -- var.elim.:  99000/381868          
c   -- var.elim.:  100000/381868          
c   -- var.elim.:  101000/381868          
c   -- var.elim.:  102000/381868          
c   -- var.elim.:  103000/381868          
c   -- var.elim.:  104000/381868          
c   -- var.elim.:  105000/381868          
c   -- var.elim.:  106000/381868          
c   -- var.elim.:  107000/381868          
c   -- var.elim.:  108000/381868          
c   -- var.elim.:  109000/381868          
c   -- var.elim.:  110000/381868          
c   -- var.elim.:  111000/381868          
c   -- var.elim.:  112000/381868          
c   -- var.elim.:  113000/381868          
c   -- var.elim.:  114000/381868          
c   -- var.elim.:  115000/381868          
c   -- var.elim.:  116000/381868          
c   -- var.elim.:  117000/381868          
c   -- var.elim.:  118000/381868          
c   -- var.elim.:  119000/381868          
c   -- var.elim.:  120000/381868          
c   -- var.elim.:  121000/381868          
c   -- var.elim.:  122000/381868          
c   -- var.elim.:  123000/381868          
c   -- var.elim.:  124000/381868          
c   -- var.elim.:  125000/381868          
c   -- var.elim.:  126000/381868          
c   -- var.elim.:  127000/381868          
c   -- var.elim.:  128000/381868          
c   -- var.elim.:  129000/381868          
c   -- var.elim.:  130000/381868          
c   -- var.elim.:  131000/381868          
c   -- var.elim.:  132000/381868          
c   -- var.elim.:  133000/381868          
c   -- var.elim.:  134000/381868          
c   -- var.elim.:  135000/381868          
c   -- var.elim.:  136000/381868          
c   -- var.elim.:  137000/381868          
c   -- var.elim.:  138000/381868          
c   -- var.elim.:  139000/381868          
c   -- var.elim.:  140000/381868          
c   -- var.elim.:  141000/381868          
c   -- var.elim.:  142000/381868          
c   -- var.elim.:  143000/381868          
c   -- var.elim.:  144000/381868          
c   -- var.elim.:  145000/381868          
c   -- var.elim.:  146000/381868          
c   -- var.elim.:  147000/381868          
c   -- var.elim.:  148000/381868          
c   -- var.elim.:  149000/381868          
c   -- var.elim.:  150000/381868          
c   -- var.elim.:  151000/381868          
c   -- var.elim.:  152000/381868          
c   -- var.elim.:  153000/381868          
c   -- var.elim.:  154000/381868          
c   -- var.elim.:  155000/381868          
c   -- var.elim.:  156000/381868          
c   -- var.elim.:  157000/381868          
c   -- var.elim.:  158000/381868          
c   -- var.elim.:  159000/381868          
c   -- var.elim.:  160000/381868          
c   -- var.elim.:  161000/381868          
c   -- var.elim.:  162000/381868          
c   -- var.elim.:  163000/381868          
c   -- var.elim.:  164000/381868          
c   -- var.elim.:  165000/381868          
c   -- var.elim.:  166000/381868          
c   -- var.elim.:  167000/381868          
c   -- var.elim.:  168000/381868          
c   -- var.elim.:  169000/381868          
c   -- var.elim.:  170000/381868          
c   -- var.elim.:  171000/381868          
c   -- var.elim.:  172000/381868          
c   -- var.elim.:  173000/381868          
c   -- var.elim.:  174000/381868          
c   -- var.elim.:  175000/381868          
c   -- var.elim.:  176000/381868          
c   -- var.elim.:  177000/381868          
c   -- var.elim.:  178000/381868          
c   -- var.elim.:  179000/381868          
c   -- var.elim.:  180000/381868          
c   -- var.elim.:  181000/381868          
c   -- var.elim.:  182000/381868          
c   -- var.elim.:  183000/381868          
c   -- var.elim.:  184000/381868          
c   -- var.elim.:  185000/381868          
c   -- var.elim.:  186000/381868          
c   -- var.elim.:  187000/381868          
c   -- var.elim.:  188000/381868          
c   -- var.elim.:  189000/381868          
c   -- var.elim.:  190000/381868          
c   -- var.elim.:  191000/381868          
c   -- var.elim.:  192000/381868          
c   -- var.elim.:  193000/381868          
c   -- var.elim.:  194000/381868          
c   -- var.elim.:  195000/381868          
c   -- var.elim.:  196000/381868          
c   -- var.elim.:  197000/381868          
c   -- var.elim.:  198000/381868          
c   -- var.elim.:  199000/381868          
c   -- var.elim.:  200000/381868          
c   -- var.elim.:  201000/381868          
c   -- var.elim.:  202000/381868          
c   -- var.elim.:  203000/381868          
c   -- var.elim.:  204000/381868          
c   -- var.elim.:  205000/381868          
c   -- var.elim.:  206000/381868          
c   -- var.elim.:  207000/381868          
c   -- var.elim.:  208000/381868          
c   -- var.elim.:  209000/381868          
c   -- var.elim.:  210000/381868          
c   -- var.elim.:  211000/381868          
c   -- var.elim.:  212000/381868          
c   -- var.elim.:  213000/381868          
c   -- var.elim.:  214000/381868          
c   -- var.elim.:  215000/381868          
c   -- var.elim.:  216000/381868          
c   -- var.elim.:  217000/381868          
c   -- var.elim.:  218000/381868          
c   -- var.elim.:  219000/381868          
c   -- var.elim.:  220000/381868          
c   -- var.elim.:  221000/381868          
c   -- var.elim.:  222000/381868          
c   -- var.elim.:  223000/381868          
c   -- var.elim.:  224000/381868          
c   -- var.elim.:  225000/381868          
c   -- var.elim.:  226000/381868          
c   -- var.elim.:  227000/381868          
c   -- var.elim.:  228000/381868          
c   -- var.elim.:  229000/381868          
c   -- var.elim.:  230000/381868          
c   -- var.elim.:  231000/381868          
c   -- var.elim.:  232000/381868          
c   -- var.elim.:  233000/381868          
c   -- var.elim.:  234000/381868          
c   -- var.elim.:  235000/381868          
c   -- var.elim.:  236000/381868          
c   -- var.elim.:  237000/381868          
c   -- var.elim.:  238000/381868          
c   -- var.elim.:  239000/381868          
c   -- var.elim.:  240000/381868          
c   -- var.elim.:  241000/381868          
c   -- var.elim.:  242000/381868          
c   -- var.elim.:  243000/381868          
c   -- var.elim.:  244000/381868          
c   -- var.elim.:  245000/381868          
c   -- var.elim.:  246000/381868          
c   -- var.elim.:  247000/381868          
c   -- var.elim.:  248000/381868          
c   -- var.elim.:  249000/381868          
c   -- var.elim.:  250000/381868          
c   -- var.elim.:  251000/381868          
c   -- var.elim.:  252000/381868          
c   -- var.elim.:  253000/381868          
c   -- var.elim.:  254000/381868          
c   -- var.elim.:  255000/381868          
c   -- var.elim.:  256000/381868          
c   -- var.elim.:  257000/381868          
c   -- var.elim.:  258000/381868          
c   -- var.elim.:  259000/381868          
c   -- var.elim.:  260000/381868          
c   -- var.elim.:  261000/381868          
c   -- var.elim.:  262000/381868          
c   -- var.elim.:  263000/381868          
c   -- var.elim.:  264000/381868          
c   -- var.elim.:  265000/381868          
c   -- var.elim.:  266000/381868          
c   -- var.elim.:  267000/381868          
c   -- var.elim.:  268000/381868          
c   -- var.elim.:  269000/381868          
c   -- var.elim.:  270000/381868          
c   -- var.elim.:  271000/381868          
c   -- var.elim.:  272000/381868          
c   -- var.elim.:  273000/381868          
c   -- var.elim.:  274000/381868          
c   -- var.elim.:  275000/381868          
c   -- var.elim.:  276000/381868          
c   -- var.elim.:  277000/381868          
c   -- var.elim.:  278000/381868          
c   -- var.elim.:  279000/381868          
c   -- var.elim.:  280000/381868          
c   -- var.elim.:  281000/381868          
c   -- var.elim.:  282000/381868          
c   -- var.elim.:  283000/381868          
c   -- var.elim.:  284000/381868          
c   -- var.elim.:  285000/381868          
c   -- var.elim.:  286000/381868          
c   -- var.elim.:  287000/381868          
c   -- var.elim.:  288000/381868          
c   -- var.elim.:  289000/381868          
c   -- var.elim.:  290000/381868          
c   -- var.elim.:  291000/381868          
c   -- var.elim.:  292000/381868          
c   -- var.elim.:  293000/381868          
c   -- var.elim.:  294000/381868          
c   -- var.elim.:  295000/381868          
c   -- var.elim.:  296000/381868          
c   -- var.elim.:  297000/381868          
c   -- var.elim.:  298000/381868          
c   -- var.elim.:  299000/381868          
c   -- var.elim.:  300000/381868          
c   -- var.elim.:  301000/381868          
c   -- var.elim.:  302000/381868          
c   -- var.elim.:  303000/381868          
c   -- var.elim.:  304000/381868          
c   -- var.elim.:  305000/381868          
c   -- var.elim.:  306000/381868          
c   -- var.elim.:  307000/381868          
c   -- var.elim.:  308000/381868          
c   -- var.elim.:  309000/381868          
c   -- var.elim.:  310000/381868          
c   -- var.elim.:  311000/381868          
c   -- var.elim.:  312000/381868          
c   -- var.elim.:  313000/381868          
c   -- var.elim.:  314000/381868          
c   -- var.elim.:  315000/381868          
c   -- var.elim.:  316000/381868          
c   -- var.elim.:  317000/381868          
c   -- var.elim.:  318000/381868          
c   -- var.elim.:  319000/381868          
c   -- var.elim.:  320000/381868          
c   -- var.elim.:  321000/381868          
c   -- var.elim.:  322000/381868          
c   -- var.elim.:  323000/381868          
c   -- var.elim.:  324000/381868          
c   -- var.elim.:  325000/381868          
c   -- var.elim.:  326000/381868          
c   -- var.elim.:  327000/381868          
c   -- var.elim.:  328000/381868          
c   -- var.elim.:  329000/381868          
c   -- var.elim.:  330000/381868          
c   -- var.elim.:  331000/381868          
c   -- var.elim.:  332000/381868          
c   -- var.elim.:  333000/381868          
c   -- var.elim.:  334000/381868          
c   -- var.elim.:  335000/381868          
c   -- var.elim.:  336000/381868          
c   -- var.elim.:  337000/381868          
c   -- var.elim.:  338000/381868          
c   -- var.elim.:  339000/381868          
c   -- var.elim.:  340000/381868          
c   -- var.elim.:  341000/381868          
c   -- var.elim.:  342000/381868          
c   -- var.elim.:  343000/381868          
c   -- var.elim.:  344000/381868          
c   -- var.elim.:  345000/381868          
c   -- var.elim.:  346000/381868          
c   -- var.elim.:  347000/381868          
c   -- var.elim.:  348000/381868          
c   -- var.elim.:  349000/381868          
c   -- var.elim.:  350000/381868          
c   -- var.elim.:  351000/381868          
c   -- var.elim.:  352000/381868          
c   -- var.elim.:  353000/381868          
c   -- var.elim.:  354000/381868          
c   -- var.elim.:  355000/381868          
c   -- var.elim.:  356000/381868          
c   -- var.elim.:  357000/381868          
c   -- var.elim.:  358000/381868          
c   -- var.elim.:  359000/381868          
c   -- var.elim.:  360000/381868          
c   -- var.elim.:  361000/381868          
c   -- var.elim.:  362000/381868          
c   -- var.elim.:  363000/381868          
c   -- var.elim.:  364000/381868          
c   -- var.elim.:  365000/381868          
c   -- var.elim.:  366000/381868          
c   -- var.elim.:  367000/381868          
c   -- var.elim.:  368000/381868          
c   -- var.elim.:  369000/381868          
c   -- var.elim.:  370000/381868          
c   -- var.elim.:  371000/381868          
c   -- var.elim.:  372000/381868          
c   -- var.elim.:  373000/381868          
c   -- var.elim.:  374000/381868          
c   -- var.elim.:  375000/381868          
c   -- var.elim.:  376000/381868          
c   -- var.elim.:  377000/381868          
c   -- var.elim.:  378000/381868          
c   -- var.elim.:  379000/381868          
c   -- var.elim.:  380000/381868          
c   -- var.elim.:  381000/381868          
c   -- var.elim.:  381868/381868          
c   -- var.elim.:  1000/2418          
c   -- var.elim.:  2000/2418          
c   -- var.elim.:  2418/2418          
c   -- subsuming                       
c   -- var.elim.:  1000/43928          
c   -- var.elim.:  2000/43928          
c   -- var.elim.:  3000/43928          
c   -- var.elim.:  4000/43928          
c   -- var.elim.:  5000/43928          
c   -- var.elim.:  6000/43928          
c   -- var.elim.:  7000/43928          
c   -- var.elim.:  8000/43928          
c   -- var.elim.:  9000/43928          
c   -- var.elim.:  10000/43928          
c   -- var.elim.:  11000/43928          
c   -- var.elim.:  12000/43928          
c   -- var.elim.:  13000/43928          
c   -- var.elim.:  14000/43928          
c   -- var.elim.:  15000/43928          
c   -- var.elim.:  16000/43928          
c   -- var.elim.:  17000/43928          
c   -- var.elim.:  18000/43928          
c   -- var.elim.:  19000/43928          
c   -- var.elim.:  20000/43928          
c   -- var.elim.:  21000/43928          
c   -- var.elim.:  22000/43928          
c   -- var.elim.:  23000/43928          
c   -- var.elim.:  24000/43928          
c   -- var.elim.:  25000/43928          
c   -- var.elim.:  26000/43928          
c   -- var.elim.:  27000/43928          
c   -- var.elim.:  28000/43928          
c   -- var.elim.:  29000/43928          
c   -- var.elim.:  30000/43928          
c   -- var.elim.:  31000/43928          
c   -- var.elim.:  32000/43928          
c   -- var.elim.:  33000/43928          
c   -- var.elim.:  34000/43928          
c   -- var.elim.:  35000/43928          
c   -- var.elim.:  36000/43928          
c   -- var.elim.:  37000/43928          
c   -- var.elim.:  38000/43928          
c   -- var.elim.:  39000/43928          
c   -- var.elim.:  40000/43928          
c   -- var.elim.:  41000/43928          
c   -- var.elim.:  42000/43928          
c   -- var.elim.:  43000/43928          
c   -- var.elim.:  43928/43928          
c   -- var.elim.:  1000/19589          
c   -- var.elim.:  2000/19589          
c   -- var.elim.:  3000/19589          
c   -- var.elim.:  4000/19589          
c   -- var.elim.:  5000/19589          
c   -- var.elim.:  6000/19589          
c   -- var.elim.:  7000/19589          
c   -- var.elim.:  8000/19589          
c   -- var.elim.:  9000/19589          
c   -- var.elim.:  10000/19589          
c   -- var.elim.:  11000/19589          
c   -- var.elim.:  12000/19589          
c   -- var.elim.:  13000/19589          
c   -- var.elim.:  14000/19589          
c   -- var.elim.:  15000/19589          
c   -- var.elim.:  16000/19589          
c   -- var.elim.:  17000/19589          
c   -- var.elim.:  18000/19589          
c   -- var.elim.:  19000/19589          
c   -- var.elim.:  19589/19589          
c   -- subsuming                       
c   -- var.elim.:  1000/15599          
c   -- var.elim.:  2000/15599          
c   -- var.elim.:  3000/15599          
c   -- var.elim.:  4000/15599          
c   -- var.elim.:  5000/15599          
c   -- var.elim.:  6000/15599          
c   -- var.elim.:  7000/15599          
c   -- var.elim.:  8000/15599          
c   -- var.elim.:  9000/15599          
c   -- var.elim.:  10000/15599          
c   -- var.elim.:  11000/15599          
c   -- var.elim.:  12000/15599          
c   -- var.elim.:  13000/15599          
c   -- var.elim.:  14000/15599          
c   -- var.elim.:  15000/15599          
c   -- var.elim.:  15599/15599          
c   -- var.elim.:  1000/5222          
c   -- var.elim.:  2000/5222          
c   -- var.elim.:  3000/5222          
c   -- var.elim.:  4000/5222          
c   -- var.elim.:  5000/5222          
c   -- var.elim.:  5222/5222          
c   -- subsuming                       
c   -- var.elim.:  1000/2675          
c   -- var.elim.:  2000/2675          
c   -- var.elim.:  2675/2675          
c |         0 | 2530533  8084025 |      --       0       --      -- |     --   | -266320/515646
c |         0 | 2530533  8084025 | 1012213       0        0     nan |  0.000 % |
c |       100 | 2530533  8084025 | 1113434     100      317     3.2 |  3.906 % |
c |       250 | 2530533  8084025 | 1224777     250      794     3.2 |  3.906 % |
c |       475 | 2530510  8083905 | 1347243     474     1807     3.8 |  3.907 % |
c |       812 | 2530510  8083905 | 1481967     811     4271     5.3 |  3.907 % |
c |      1318 | 2530510  8083905 | 1630164    1317     6957     5.3 |  3.907 % |
c |      2077 | 2530510  8083905 | 1793181    2076    12232     5.9 |  3.907 % |
c |      3216 | 2530510  8083905 | 1972499    3215    18166     5.7 |  3.907 % |
c |      4925 | 2530380  8083467 | 2169637    4923    28352     5.8 |  3.910 % |
c |      7487 | 2530327  8083196 | 2386551    7483    49859     6.7 |  3.912 % |
c |     11333 | 2530280  8082988 | 2625157   11328    88000     7.8 |  3.913 % |
c |     17101 | 2529854  8081545 | 2887187   17091   165857     9.7 |  3.924 % |
c |     25750 | 2528809#### 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.93 0.98 0.92 2/54 32086
Raw data (stat): 32086 (runsolver) R 32085 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484594617 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99982 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 15203 0 0 0 960 38 0 0 25 0 1 0 484594617 57221120 12363 4294967295 134512640 134672761 3221224544 3221222732 1075350746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13970 12363 603 41 0 13929 0
vsize: 55880
[startup+20.0005 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 54157 0 0 0 1864 134 0 0 25 0 1 0 484594617 236339200 51317 4294967295 134512640 134672761 3221224544 3221202996 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57700 51317 603 41 0 57659 0
vsize: 230800
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 107903 0 0 0 2727 271 0 0 25 0 1 0 484594617 490602496 105063 4294967295 134512640 134672761 3221224544 3221215904 134604223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119776 105063 603 41 0 119735 0
vsize: 479104
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 126591 0 0 0 3676 322 0 0 25 0 1 0 484594617 551358464 123751 4294967295 134512640 134672761 3221224544 3221223088 134621044 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134609 123751 603 41 0 134568 0
vsize: 538436
[startup+50.0022 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 130986 0 0 0 4667 331 0 0 25 0 1 0 484594617 559747072 125414 4294967295 134512640 134672761 3221224544 3221223104 134645817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136657 125414 603 41 0 136616 0
vsize: 546628
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 132750 0 0 0 5642 356 0 0 25 0 1 0 484594617 560001024 125547 4294967295 134512640 134672761 3221224544 3221222632 134566425 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 136719 125547 603 41 0 136678 0
vsize: 546876
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 132867 0 0 0 6624 374 0 0 25 0 1 0 484594617 560406528 125664 4294967295 134512640 134672761 3221224544 3221222752 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136818 125664 603 41 0 136777 0
vsize: 547272
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 133052 0 0 0 7604 394 0 0 25 0 1 0 484594617 560947200 125849 4294967295 134512640 134672761 3221224544 3221222752 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136950 125849 603 41 0 136909 0
vsize: 547800
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 133319 0 0 0 8583 416 0 0 25 0 1 0 484594617 561893376 126116 4294967295 134512640 134672761 3221224544 3221222936 1075280261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137181 126116 603 41 0 137140 0
vsize: 548724
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 133770 0 0 0 9576 422 0 0 25 0 1 0 484594617 560996352 125770 4294967295 134512640 134672761 3221224544 3221223036 134638243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136962 125770 603 41 0 136921 0
vsize: 547848
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 133770 0 0 0 10577 422 0 0 25 0 1 0 484594617 560996352 125770 4294967295 134512640 134672761 3221224544 3221222992 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136962 125770 603 41 0 136921 0
vsize: 547848
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 141491 0 0 0 11559 440 0 0 25 0 1 0 484594617 613687296 132229 4294967295 134512640 134672761 3221224544 3221223012 1075351087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149826 132229 603 41 0 149785 0
vsize: 599304
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 141720 0 0 0 12557 442 0 0 25 0 1 0 484594617 556388352 124739 4294967295 134512640 134672761 3221224544 3221223004 134643896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135837 124739 603 41 0 135796 0
vsize: 543348
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 151831 0 0 0 13532 467 0 0 25 0 1 0 484594617 556212224 124728 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135794 124728 603 41 0 135753 0
vsize: 543176
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 151856 0 0 0 14532 467 0 0 25 0 1 0 484594617 556617728 124753 4294967295 134512640 134672761 3221224544 3221223668 134566151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135893 124753 603 41 0 135852 0
vsize: 543572
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 151896 0 0 0 15532 468 0 0 25 0 1 0 484594617 556617728 124793 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135893 124793 603 41 0 135852 0
vsize: 543572
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 151942 0 0 0 16532 468 0 0 25 0 1 0 484594617 556871680 124839 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135955 124839 603 41 0 135914 0
vsize: 543820
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 151968 0 0 0 17532 468 0 0 25 0 1 0 484594617 556871680 124865 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135955 124865 603 41 0 135914 0
vsize: 543820
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152013 0 0 0 18532 468 0 0 25 0 1 0 484594617 557133824 124910 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136019 124910 603 41 0 135978 0
vsize: 544076
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152015 0 0 0 19532 468 0 0 25 0 1 0 484594617 557133824 124912 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136019 124912 603 41 0 135978 0
vsize: 544076
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152019 0 0 0 20533 468 0 0 25 0 1 0 484594617 557133824 124916 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136019 124916 603 41 0 135978 0
vsize: 544076
[startup+220.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152072 0 0 0 21533 468 0 0 25 0 1 0 484594617 557920256 124969 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136211 124969 603 41 0 136170 0
vsize: 544844
[startup+230.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152073 0 0 0 22533 468 0 0 25 0 1 0 484594617 557920256 124970 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136211 124970 603 41 0 136170 0
vsize: 544844
[startup+240.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152078 0 0 0 23533 468 0 0 25 0 1 0 484594617 557920256 124975 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136211 124975 603 41 0 136170 0
vsize: 544844
[startup+250.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152085 0 0 0 24533 468 0 0 25 0 1 0 484594617 557920256 124982 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136211 124982 603 41 0 136170 0
vsize: 544844
[startup+260.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152090 0 0 0 25533 468 0 0 25 0 1 0 484594617 557920256 124987 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136211 124987 603 41 0 136170 0
vsize: 544844
[startup+270.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152099 0 0 0 26533 468 0 0 25 0 1 0 484594617 557920256 124996 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136211 124996 603 41 0 136170 0
vsize: 544844
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152105 0 0 0 27533 468 0 0 25 0 1 0 484594617 557920256 125002 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136211 125002 603 41 0 136170 0
vsize: 544844
[startup+290.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152113 0 0 0 28534 468 0 0 25 0 1 0 484594617 557920256 125010 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136211 125010 603 41 0 136170 0
vsize: 544844
[startup+300.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152131 0 0 0 29534 468 0 0 25 0 1 0 484594617 558055424 125028 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136244 125028 603 41 0 136203 0
vsize: 544976
[startup+310.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152226 0 0 0 30534 469 0 0 25 0 1 0 484594617 558456832 125123 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136342 125123 603 41 0 136301 0
vsize: 545368
[startup+320.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152272 0 0 0 31534 469 0 0 25 0 1 0 484594617 558592000 125169 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136375 125169 603 41 0 136334 0
vsize: 545500
[startup+330.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152339 0 0 0 32534 469 0 0 25 0 1 0 484594617 558985216 125236 4294967295 134512640 134672761 3221224544 3221223728 134615845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136471 125236 603 41 0 136430 0
vsize: 545884
[startup+340.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152404 0 0 0 33534 469 0 0 25 0 1 0 484594617 559247360 125301 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136535 125301 603 41 0 136494 0
vsize: 546140
[startup+350.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152419 0 0 0 34534 469 0 0 25 0 1 0 484594617 559382528 125316 4294967295 134512640 134672761 3221224544 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136568 125316 603 41 0 136527 0
vsize: 546272
[startup+360.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152429 0 0 0 35534 469 0 0 25 0 1 0 484594617 559382528 125326 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136568 125326 603 41 0 136527 0
vsize: 546272
[startup+370.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152448 0 0 0 36534 469 0 0 25 0 1 0 484594617 559382528 125345 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136568 125345 603 41 0 136527 0
vsize: 546272
[startup+380.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152472 0 0 0 37534 469 0 0 25 0 1 0 484594617 559517696 125369 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136601 125369 603 41 0 136560 0
vsize: 546404
[startup+390.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152513 0 0 0 38534 469 0 0 25 0 1 0 484594617 559648768 125410 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136633 125410 603 41 0 136592 0
vsize: 546532
[startup+400.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152538 0 0 0 39535 469 0 0 25 0 1 0 484594617 559783936 125435 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136666 125435 603 41 0 136625 0
vsize: 546664
[startup+410.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152571 0 0 0 40535 469 0 0 25 0 1 0 484594617 559919104 125468 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136699 125468 603 41 0 136658 0
vsize: 546796
[startup+420.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152608 0 0 0 41535 469 0 0 25 0 1 0 484594617 560054272 125505 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136732 125505 603 41 0 136691 0
vsize: 546928
[startup+430.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 152643 0 0 0 42535 469 0 0 25 0 1 0 484594617 560185344 125540 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136764 125540 603 41 0 136723 0
vsize: 547056
[startup+440.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 153218 0 0 0 43534 471 0 0 25 0 1 0 484594617 562429952 126115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137312 126115 603 41 0 137271 0
vsize: 549248
[startup+450.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 153634 0 0 0 44532 472 0 0 25 0 1 0 484594617 564137984 126531 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137729 126531 603 41 0 137688 0
vsize: 550916
[startup+460.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 153981 0 0 0 45531 474 0 0 25 0 1 0 484594617 565592064 126878 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138084 126878 603 41 0 138043 0
vsize: 552336
[startup+470.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 154327 0 0 0 46530 475 0 0 25 0 1 0 484594617 567083008 127224 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138448 127224 603 41 0 138407 0
vsize: 553792
[startup+480.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 154583 0 0 0 47530 475 0 0 25 0 1 0 484594617 568000512 127480 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138672 127480 603 41 0 138631 0
vsize: 554688
[startup+490.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 154807 0 0 0 48529 476 0 0 25 0 1 0 484594617 568930304 127704 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138899 127704 603 41 0 138858 0
vsize: 555596
[startup+500.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155041 0 0 0 49530 477 0 0 25 0 1 0 484594617 570437632 127938 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139267 127938 603 41 0 139226 0
vsize: 557068
[startup+510.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155073 0 0 0 50530 477 0 0 25 0 1 0 484594617 570580992 127970 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139302 127970 603 41 0 139261 0
vsize: 557208
[startup+520.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155104 0 0 0 51530 477 0 0 25 0 1 0 484594617 570716160 128001 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139335 128001 603 41 0 139294 0
vsize: 557340
[startup+530.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155162 0 0 0 52530 477 0 0 25 0 1 0 484594617 570847232 128059 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139367 128059 603 41 0 139326 0
vsize: 557468
[startup+540.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155488 0 0 0 53529 478 0 0 25 0 1 0 484594617 572166144 128385 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139689 128385 603 41 0 139648 0
vsize: 558756
[startup+550.009 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155539 0 0 0 54529 478 0 0 25 0 1 0 484594617 572436480 128436 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139755 128436 603 41 0 139714 0
vsize: 559020
[startup+560.009 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155570 0 0 0 55529 478 0 0 25 0 1 0 484594617 572436480 128467 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139755 128467 603 41 0 139714 0
vsize: 559020
[startup+570.009 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155591 0 0 0 56529 478 0 0 25 0 1 0 484594617 572567552 128488 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139787 128488 603 41 0 139746 0
vsize: 559148
[startup+580.009 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155618 0 0 0 57529 478 0 0 25 0 1 0 484594617 572702720 128515 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139820 128515 603 41 0 139779 0
vsize: 559280
[startup+590.01 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155641 0 0 0 58529 479 0 0 25 0 1 0 484594617 572702720 128538 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139820 128538 603 41 0 139779 0
vsize: 559280
[startup+600.01 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155760 0 0 0 59529 479 0 0 25 0 1 0 484594617 573231104 128657 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139949 128657 603 41 0 139908 0
vsize: 559796
[startup+610.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155823 0 0 0 60529 479 0 0 25 0 1 0 484594617 573493248 128720 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140013 128720 603 41 0 139972 0
vsize: 560052
[startup+620.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155864 0 0 0 61530 479 0 0 25 0 1 0 484594617 573624320 128761 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140045 128761 603 41 0 140004 0
vsize: 560180
[startup+630.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155879 0 0 0 62530 479 0 0 25 0 1 0 484594617 573624320 128776 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140045 128776 603 41 0 140004 0
vsize: 560180
[startup+640.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155969 0 0 0 63530 479 0 0 25 0 1 0 484594617 574017536 128866 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140141 128866 603 41 0 140100 0
vsize: 560564
[startup+650.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 155995 0 0 0 64530 479 0 0 25 0 1 0 484594617 574169088 128892 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140178 128892 603 41 0 140137 0
vsize: 560712
[startup+660.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156025 0 0 0 65530 479 0 0 25 0 1 0 484594617 574169088 128922 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140178 128922 603 41 0 140137 0
vsize: 560712
[startup+670.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156042 0 0 0 66530 480 0 0 25 0 1 0 484594617 574304256 128939 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140211 128939 603 41 0 140170 0
vsize: 560844
[startup+680.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156069 0 0 0 67530 480 0 0 25 0 1 0 484594617 574439424 128966 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140244 128966 603 41 0 140203 0
vsize: 560976
[startup+690.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156093 0 0 0 68530 480 0 0 25 0 1 0 484594617 574439424 128990 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140244 128990 603 41 0 140203 0
vsize: 560976
[startup+700.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156133 0 0 0 69530 480 0 0 25 0 1 0 484594617 574574592 129030 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140277 129030 603 41 0 140236 0
vsize: 561108
[startup+710.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156149 0 0 0 70530 480 0 0 25 0 1 0 484594617 574574592 129046 4294967295 134512640 134672761 3221224544 3221223680 134614816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140277 129046 603 41 0 140236 0
vsize: 561108
[startup+720.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156179 0 0 0 71530 480 0 0 25 0 1 0 484594617 574709760 129076 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140310 129076 603 41 0 140269 0
vsize: 561240
[startup+730.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156212 0 0 0 72530 480 0 0 25 0 1 0 484594617 575107072 129109 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140407 129109 603 41 0 140366 0
vsize: 561628
[startup+740.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156251 0 0 0 73531 481 0 0 25 0 1 0 484594617 575242240 129148 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140440 129148 603 41 0 140399 0
vsize: 561760
[startup+750.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156295 0 0 0 74531 481 0 0 25 0 1 0 484594617 575377408 129192 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140473 129192 603 41 0 140432 0
vsize: 561892
[startup+760.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156314 0 0 0 75531 481 0 0 25 0 1 0 484594617 575512576 129211 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140506 129211 603 41 0 140465 0
vsize: 562024
[startup+770.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156336 0 0 0 76531 481 0 0 25 0 1 0 484594617 575512576 129233 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140506 129233 603 41 0 140465 0
vsize: 562024
[startup+780.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156357 0 0 0 77531 481 0 0 25 0 1 0 484594617 575643648 129254 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140538 129254 603 41 0 140497 0
vsize: 562152
[startup+790.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156376 0 0 0 78531 481 0 0 25 0 1 0 484594617 575643648 129273 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140538 129273 603 41 0 140497 0
vsize: 562152
[startup+800.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156409 0 0 0 79532 481 0 0 25 0 1 0 484594617 575778816 129306 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140571 129306 603 41 0 140530 0
vsize: 562284
[startup+810.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156428 0 0 0 80532 481 0 0 25 0 1 0 484594617 575913984 129325 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140604 129325 603 41 0 140563 0
vsize: 562416
[startup+820.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156508 0 0 0 81531 481 0 0 25 0 1 0 484594617 576180224 129405 4294967295 134512640 134672761 3221224544 3221223688 134616261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140669 129405 603 41 0 140628 0
vsize: 562676
[startup+830.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156565 0 0 0 82531 482 0 0 25 0 1 0 484594617 576315392 129462 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140702 129462 603 41 0 140661 0
vsize: 562808
[startup+840.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156615 0 0 0 83531 482 0 0 25 0 1 0 484594617 576581632 129512 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140767 129512 603 41 0 140726 0
vsize: 563068
[startup+850.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 156992 0 0 0 84532 482 0 0 25 0 1 0 484594617 578031616 129889 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141121 129889 603 41 0 141080 0
vsize: 564484
[startup+860.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157033 0 0 0 85532 482 0 0 25 0 1 0 484594617 578166784 129930 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141154 129930 603 41 0 141113 0
vsize: 564616
[startup+870.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157059 0 0 0 86532 482 0 0 25 0 1 0 484594617 578301952 129956 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141187 129956 603 41 0 141146 0
vsize: 564748
[startup+880.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157080 0 0 0 87535 482 0 0 25 0 1 0 484594617 578437120 129977 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141220 129977 603 41 0 141179 0
vsize: 564880
[startup+890.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157315 0 0 0 88536 483 0 0 25 0 1 0 484594617 579362816 130212 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141446 130212 603 41 0 141405 0
vsize: 565784
[startup+900.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157379 0 0 0 89536 483 0 0 25 0 1 0 484594617 579629056 130276 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141511 130276 603 41 0 141470 0
vsize: 566044
[startup+910.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157398 0 0 0 90537 484 0 0 25 0 1 0 484594617 579629056 130295 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141511 130295 603 41 0 141470 0
vsize: 566044
[startup+920.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157415 0 0 0 91537 484 0 0 25 0 1 0 484594617 579764224 130312 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141544 130312 603 41 0 141503 0
vsize: 566176
[startup+930.081 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157427 0 0 0 92537 484 0 0 25 0 1 0 484594617 579764224 130324 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141544 130324 603 41 0 141503 0
vsize: 566176
[startup+940.082 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157443 0 0 0 93538 484 0 0 25 0 1 0 484594617 579764224 130340 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141544 130340 603 41 0 141503 0
vsize: 566176
[startup+950.091 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157463 0 0 0 94539 484 0 0 25 0 1 0 484594617 579895296 130360 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141576 130360 603 41 0 141535 0
vsize: 566304
[startup+960.096 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157478 0 0 0 95539 484 0 0 25 0 1 0 484594617 579895296 130375 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141576 130375 603 41 0 141535 0
vsize: 566304
[startup+970.096 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157536 0 0 0 96539 484 0 0 25 0 1 0 484594617 580165632 130433 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141642 130433 603 41 0 141601 0
vsize: 566568
[startup+980.095 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157556 0 0 0 97539 484 0 0 25 0 1 0 484594617 580300800 130453 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141675 130453 603 41 0 141634 0
vsize: 566700
[startup+990.096 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157582 0 0 0 98540 484 0 0 25 0 1 0 484594617 580300800 130479 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141675 130479 603 41 0 141634 0
vsize: 566700
[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157610 0 0 0 99540 484 0 0 25 0 1 0 484594617 580431872 130507 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141707 130507 603 41 0 141666 0
vsize: 566828
[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157636 0 0 0 100540 485 0 0 25 0 1 0 484594617 581611520 130533 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141995 130533 603 41 0 141954 0
vsize: 567980
[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157659 0 0 0 101540 485 0 0 25 0 1 0 484594617 581611520 130556 4294967295 134512640 134672761 3221224544 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141995 130556 603 41 0 141954 0
vsize: 567980
[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157672 0 0 0 102540 485 0 0 25 0 1 0 484594617 581746688 130569 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142028 130569 603 41 0 141987 0
vsize: 568112
[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157685 0 0 0 103540 485 0 0 25 0 1 0 484594617 581746688 130582 4294967295 134512640 134672761 3221224544 3221223728 134610778 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142028 130582 603 41 0 141987 0
vsize: 568112
[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157698 0 0 0 104540 485 0 0 25 0 1 0 484594617 581746688 130595 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142028 130595 603 41 0 141987 0
vsize: 568112
[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157711 0 0 0 105540 485 0 0 25 0 1 0 484594617 581881856 130608 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142061 130608 603 41 0 142020 0
vsize: 568244
[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157722 0 0 0 106541 485 0 0 25 0 1 0 484594617 581881856 130619 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142061 130619 603 41 0 142020 0
vsize: 568244
[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157737 0 0 0 107541 485 0 0 25 0 1 0 484594617 581881856 130634 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142061 130634 603 41 0 142020 0
vsize: 568244
[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157767 0 0 0 108541 485 0 0 25 0 1 0 484594617 582017024 130664 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142094 130664 603 41 0 142053 0
vsize: 568376
[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157777 0 0 0 109541 485 0 0 25 0 1 0 484594617 582017024 130674 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142094 130674 603 41 0 142053 0
vsize: 568376
[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157783 0 0 0 110541 485 0 0 25 0 1 0 484594617 582017024 130680 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142094 130680 603 41 0 142053 0
vsize: 568376
[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157798 0 0 0 111541 485 0 0 25 0 1 0 484594617 582148096 130695 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142126 130695 603 41 0 142085 0
vsize: 568504
[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157809 0 0 0 112542 485 0 0 25 0 1 0 484594617 582148096 130706 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142126 130706 603 41 0 142085 0
vsize: 568504
[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157818 0 0 0 113542 485 0 0 25 0 1 0 484594617 582148096 130715 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142126 130715 603 41 0 142085 0
vsize: 568504
[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157829 0 0 0 114542 485 0 0 25 0 1 0 484594617 582283264 130726 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142159 130726 603 41 0 142118 0
vsize: 568636
[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157844 0 0 0 115542 485 0 0 25 0 1 0 484594617 582283264 130741 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142159 130741 603 41 0 142118 0
vsize: 568636
[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157871 0 0 0 116542 485 0 0 25 0 1 0 484594617 582414336 130768 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142191 130768 603 41 0 142150 0
vsize: 568764
[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157887 0 0 0 117542 485 0 0 25 0 1 0 484594617 582414336 130784 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142191 130784 603 41 0 142150 0
vsize: 568764
[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157902 0 0 0 118543 486 0 0 25 0 1 0 484594617 582549504 130799 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142224 130799 603 41 0 142183 0
vsize: 568896
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 32086
Raw data (stat): 32086 (minisat+) R 32085 30701 30700 0 -1 0 157917 0 0 0 119543 486 0 0 25 0 1 0 484594617 582549504 130814 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142224 130814 603 41 0 142183 0
vsize: 568896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.42 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 32086
Raw data (stat): 32086 (minisat+) Z 32085 30701 30700 0 -1 12 157917 0 0 0 119543 517 0 0 25 0 1 0 484594617 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.42
CPU time (s): 1200.61
CPU user time (s): 1195.43
CPU system time (s): 5.17421
CPU usage (%): 100.016
Max. virtual memory (Kb): 599304
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####