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 19622

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        872048 kB
Buffers:          8080 kB
Cached:         132136 kB
SwapCached:          0 kB
Active:          53864 kB
Inactive:        89272 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        871796 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13612 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 19:45:41 (client local time) WITH STATUS 0 IN 1200.45 SECONDS
stats: 16320 7 1200.45 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1503 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssss
c ---[1507]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1506]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1505]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1504]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1503]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1502]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1501]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1500]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1499]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1498]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1497]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1496]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1495]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1494]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1493]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1492]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1491]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1490]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1489]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1488]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1487]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1486]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1485]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1484]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1483]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1482]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1481]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1480]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1479]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1478]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1477]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1476]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1475]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1474]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1473]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1472]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1471]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1470]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1469]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1468]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1467]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1466]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1465]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1464]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1463]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1462]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1461]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1460]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1459]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1458]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1457]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1456]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1455]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1454]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1453]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1452]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1451]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1450]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1449]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1448]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1447]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1446]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1445]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1444]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1443]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1442]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1441]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1440]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1439]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1438]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1437]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1436]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1435]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1434]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1433]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1432]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1431]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1430]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1429]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1428]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1427]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1426]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1425]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1424]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1423]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1422]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1421]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1420]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1419]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1418]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1417]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1416]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1415]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1414]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1413]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1412]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1411]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1410]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1409]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1408]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1407]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1406]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1405]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1404]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1403]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1402]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1401]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1400]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1399]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1398]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1397]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1396]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1395]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1394]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1393]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1392]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1391]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1390]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1389]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1388]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1387]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1386]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1385]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1384]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1383]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1382]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1381]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1380]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1379]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1378]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1377]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1376]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1375]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1374]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1373]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1372]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1371]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1370]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1369]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1368]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1367]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1366]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1365]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1364]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1363]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1362]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1361]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1360]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1359]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1358]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1357]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1356]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1355]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1354]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1353]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1352]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1351]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1350]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1349]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1348]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1347]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1346]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1345]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1344]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1343]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1342]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1341]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1340]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1339]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1338]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1337]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1336]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1335]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1334]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1333]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1332]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1331]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1330]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1329]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1328]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1327]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1326]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1325]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1324]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1323]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1322]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1321]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1320]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1319]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1318]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1317]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1316]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1315]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1314]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1313]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1312]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1311]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1310]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1309]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1308]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1307]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1306]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1305]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1304]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1303]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1302]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1301]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1300]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1299]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1298]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1297]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1296]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1295]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1294]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1293]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1292]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1291]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1290]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1289]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1288]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1287]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1286]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1285]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1284]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1283]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1282]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1281]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1280]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1279]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1278]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1277]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1276]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1275]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1274]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1273]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1272]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1271]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1270]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1269]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1268]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1267]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1266]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1265]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1264]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1263]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1262]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1261]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1260]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1259]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1258]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1257]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1256]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1255]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1254]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1253]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1252]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1251]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1250]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1249]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1248]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1247]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1246]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1245]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1244]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1243]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1242]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1241]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1240]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1239]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1238]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1237]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1236]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1235]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1234]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1233]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1232]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1231]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1230]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1229]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1228]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1227]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1226]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1225]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1224]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1222]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1221]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1220]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1218]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1217]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1216]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1215]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1214]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1213]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1212]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1211]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1210]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1209]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1208]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1207]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1206]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1205]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1204]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1203]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1202]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1201]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1200]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1199]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1198]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1197]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1196]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1195]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1194]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1193]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1192]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1191]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1190]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1189]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1188]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1187]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1186]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1185]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1184]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1183]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1182]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1181]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1180]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1179]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1178]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1177]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1176]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1175]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1174]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1173]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1172]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1171]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1170]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1169]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1168]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1167]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1166]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1165]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1163]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1162]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1161]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1160]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1158]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1157]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1156]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1155]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1154]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1153]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1152]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1151]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1150]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1149]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1148]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1147]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1145]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1144]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1143]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1142]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1141]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1140]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1139]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1138]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1137]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1136]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1134]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1133]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1132]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1130]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1129]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1128]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1127]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1126]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1125]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1124]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1123]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1122]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1121]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1120]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1119]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1118]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1117]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1116]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1115]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1114]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1113]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1112]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1111]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1110]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1109]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1108]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1107]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1106]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1105]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1103]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1102]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1101]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1100]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1099]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1098]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1097]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1096]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1095]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1094]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1093]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1092]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1091]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1090]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1089]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1088]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1087]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1086]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1085]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1083]---> BDD-cost:   76
c ---[1081]---> BDD-cost:   76
c ---[1079]---> BDD-cost:   76
c ---[1077]---> BDD-cost:   76
c ---[1075]---> BDD-cost:   76
c ---[1073]---> BDD-cost:   76
c ---[1071]---> BDD-cost:   76
c ---[1069]---> BDD-cost:   76
c ---[1067]---> BDD-cost:   76
c ---[1065]---> BDD-cost:   76
c ---[1063]---> BDD-cost:   76
c ---[1061]---> BDD-cost:   76
c ---[1059]---> BDD-cost:   76
c ---[1057]---> BDD-cost:   76
c ---[1055]---> BDD-cost:   76
c ---[1053]---> BDD-cost:   76
c ---[1051]---> BDD-cost:   76
c ---[1049]---> BDD-cost:   76
c ---[1047]---> BDD-cost:   76
c ---[1045]---> BDD-cost:   76
c ---[1043]---> BDD-cost:   76
c ---[1041]---> BDD-cost:   76
c ---[1039]---> BDD-cost:   76
c ---[1037]---> BDD-cost:   76
c ---[1035]---> BDD-cost:   76
c ---[1033]---> BDD-cost:   76
c ---[1031]---> BDD-cost:   76
c ---[1029]---> BDD-cost:   76
c ---[1027]---> BDD-cost:   76
c ---[1025]---> BDD-cost:   76
c ---[1023]---> BDD-cost:   76
c ---[1021]---> BDD-cost:   76
c ---[1019]---> BDD-cost:   76
c ---[1017]---> BDD-cost:   76
c ---[1015]---> BDD-cost:   76
c ---[1013]---> BDD-cost:   76
c ---[1011]---> BDD-cost:   76
c ---[1009]---> BDD-cost:   76
c ---[1007]---> BDD-cost:   76
c ---[1005]---> BDD-cost:   76
c ---[1003]---> BDD-cost:   76
c ---[1001]---> BDD-cost:   76
c ---[ 999]---> BDD-cost:   76
c ---[ 997]---> BDD-cost:   76
c ---[ 995]---> BDD-cost:   76
c ---[ 993]---> BDD-cost:   76
c ---[ 991]---> BDD-cost:   76
c ---[ 989]---> BDD-cost:   76
c ---[ 987]---> BDD-cost:   76
c ---[ 985]---> BDD-cost:   76
c ---[ 983]---> BDD-cost:   76
c ---[ 981]---> BDD-cost:   76
c ---[ 979]---> BDD-cost:   76
c ---[ 977]---> BDD-cost:   76
c ---[ 975]---> BDD-cost:   76
c ---[ 973]---> BDD-cost:   76
c ---[ 971]---> BDD-cost:   76
c ---[ 969]---> BDD-cost:   76
c ---[ 967]---> BDD-cost:   76
c ---[ 965]---> BDD-cost:   76
c ---[ 963]---> BDD-cost:   76
c ---[ 961]---> BDD-cost:   76
c ---[ 959]---> BDD-cost:   76
c ---[ 957]---> BDD-cost:   76
c ---[ 955]---> BDD-cost:   76
c ---[ 953]---> BDD-cost:   76
c ---[ 951]---> BDD-cost:   76
c ---[ 949]---> BDD-cost:   76
c ---[ 947]---> BDD-cost:   76
c ---[ 945]---> BDD-cost:   76
c ---[ 943]---> BDD-cost:   76
c ---[ 941]---> BDD-cost:   76
c ---[ 939]---> BDD-cost:   76
c ---[ 937]---> BDD-cost:   76
c ---[ 935]---> BDD-cost:   76
c ---[ 933]---> BDD-cost:   76
c ---[ 931]---> BDD-cost:   76
c ---[ 929]---> BDD-cost:   76
c ---[ 927]---> BDD-cost:   76
c ---[ 925]---> BDD-cost:   76
c ---[ 923]---> BDD-cost:   76
c ---[ 921]---> BDD-cost:   76
c ---[ 919]---> BDD-cost:   76
c ---[ 917]---> BDD-cost:   76
c ---[ 915]---> BDD-cost:   76
c ---[ 913]---> BDD-cost:   76
c ---[ 911]---> BDD-cost:   76
c ---[ 909]---> BDD-cost:   76
c ---[ 907]---> BDD-cost:   76
c ---[ 905]---> BDD-cost:   76
c ---[ 903]---> BDD-cost:   76
c ---[ 901]---> BDD-cost:   76
c ---[ 899]---> BDD-cost:   76
c ---[ 897]---> BDD-cost:   76
c ---[ 895]---> BDD-cost:   76
c ---[ 893]---> BDD-cost:   76
c ---[ 891]---> BDD-cost:   76
c ---[ 889]---> BDD-cost:   76
c ---[ 887]---> BDD-cost:   76
c ---[ 885]---> BDD-cost:   76
c ---[ 883]---> BDD-cost:   76
c ---[ 881]---> BDD-cost:   76
c ---[ 879]---> BDD-cost:   76
c ---[ 877]---> BDD-cost:   76
c ---[ 875]---> BDD-cost:   76
c ---[ 873]---> BDD-cost:   76
c ---[ 871]---> BDD-cost:   76
c ---[ 869]---> BDD-cost:   76
c ---[ 867]---> BDD-cost:   76
c ---[ 865]---> BDD-cost:   76
c ---[ 863]---> BDD-cost:   76
c ---[ 861]---> BDD-cost:   76
c ---[ 859]---> BDD-cost:   76
c ---[ 857]---> BDD-cost:   76
c ---[ 855]---> BDD-cost:   76
c ---[ 853]---> BDD-cost:   76
c ---[ 851]---> BDD-cost:   76
c ---[ 849]---> BDD-cost:   76
c ---[ 847]---> BDD-cost:   76
c ---[ 845]---> BDD-cost:   76
c ---[ 843]---> BDD-cost:   76
c ---[ 841]---> BDD-cost:   76
c ---[ 839]---> BDD-cost:   76
c ---[ 837]---> BDD-cost:   76
c ---[ 835]---> BDD-cost:   76
c ---[ 833]---> BDD-cost:   76
c ---[ 831]---> BDD-cost:   76
c ---[ 829]---> BDD-cost:   76
c ---[ 827]---> BDD-cost:   76
c ---[ 825]---> BDD-cost:   76
c ---[ 823]---> BDD-cost:   76
c ---[ 821]---> BDD-cost:   76
c ---[ 819]---> BDD-cost:   76
c ---[ 817]---> BDD-cost:   76
c ---[ 815]---> BDD-cost:   76
c ---[ 813]---> BDD-cost:   76
c ---[ 811]---> BDD-cost:   76
c ---[ 809]---> BDD-cost:   76
c ---[ 807]---> BDD-cost:   76
c ---[ 805]---> BDD-cost:   76
c ---[ 803]---> BDD-cost:   76
c ---[ 801]---> BDD-cost:   76
c ---[ 799]---> BDD-cost:   76
c ---[ 797]---> BDD-cost:   76
c ---[ 795]---> BDD-cost:   76
c ---[ 793]---> BDD-cost:   76
c ---[ 791]---> BDD-cost:   76
c ---[ 789]---> BDD-cost:   76
c ---[ 787]---> BDD-cost:   76
c ---[ 785]---> BDD-cost:   76
c ---[ 783]---> BDD-cost:   76
c ---[ 781]---> BDD-cost:   76
c ---[ 779]---> BDD-cost:   76
c ---[ 777]---> BDD-cost:   76
c ---[ 775]---> BDD-cost:   76
c ---[ 773]---> BDD-cost:   76
c ---[ 771]---> BDD-cost:   76
c ---[ 769]---> BDD-cost:   76
c ---[ 767]---> BDD-cost:   76
c ---[ 765]---> BDD-cost:   76
c ---[ 763]---> BDD-cost:   76
c ---[ 761]---> BDD-cost:   76
c ---[ 759]---> BDD-cost:   76
c ---[ 757]---> BDD-cost:   76
c ---[ 755]---> BDD-cost:   76
c ---[ 753]---> BDD-cost:   76
c ---[ 751]---> BDD-cost:   76
c ---[ 749]---> BDD-cost:   76
c ---[ 747]---> BDD-cost:   76
c ---[ 745]---> BDD-cost:   76
c ---[ 743]---> BDD-cost:   76
c ---[ 741]---> BDD-cost:   76
c ---[ 739]---> BDD-cost:   76
c ---[ 737]---> BDD-cost:   76
c ---[ 735]---> BDD-cost:   76
c ---[ 733]---> BDD-cost:   76
c ---[ 731]---> BDD-cost:   76
c ---[ 729]---> BDD-cost:   76
c ---[ 727]---> BDD-cost:   76
c ---[ 725]---> BDD-cost:   76
c ---[ 723]---> BDD-cost:   76
c ---[ 721]---> BDD-cost:   76
c ---[ 719]---> BDD-cost:   76
c ---[ 717]---> BDD-cost:   76
c ---[ 715]---> BDD-cost:   76
c ---[ 713]---> BDD-cost:   76
c ---[ 711]---> BDD-cost:   76
c ---[ 709]---> BDD-cost:   76
c ---[ 707]---> BDD-cost:   76
c ---[ 705]---> BDD-cost:   76
c ---[ 703]---> BDD-cost:   76
c ---[ 701]---> BDD-cost:   76
c ---[ 699]---> BDD-cost:   76
c ---[ 697]---> BDD-cost:   76
c ---[ 695]---> BDD-cost:   76
c ---[ 693]---> BDD-cost:   76
c ---[ 691]---> BDD-cost:   76
c ---[ 689]---> BDD-cost:   76
c ---[ 687]---> BDD-cost:   76
c ---[ 685]---> BDD-cost:   76
c ---[ 683]---> BDD-cost:   76
c ---[ 681]---> BDD-cost:   76
c ---[ 679]---> BDD-cost:   76
c ---[ 677]---> BDD-cost:   76
c ---[ 675]---> BDD-cost:   76
c ---[ 673]---> BDD-cost:   76
c ---[ 671]---> BDD-cost:   76
c ---[ 669]---> BDD-cost:   76
c ---[ 667]---> BDD-cost:   76
c ---[ 665]---> BDD-cost:   76
c ---[ 663]---> BDD-cost:   74
c ---[ 661]---> BDD-cost:   76
c ---[ 659]---> BDD-cost:   74
c ---[ 657]---> BDD-cost:   74
c ---[ 655]---> BDD-cost:   74
c ---[ 653]---> BDD-cost:   74
c ---[ 651]---> BDD-cost:   74
c ---[ 649]---> BDD-cost:   74
c ---[ 647]---> BDD-cost:   74
c ---[ 645]---> BDD-cost:   74
c ---[ 643]---> BDD-cost:   74
c ---[ 641]---> BDD-cost:   76
c ---[ 639]---> BDD-cost:   74
c ---[ 637]---> BDD-cost:   74
c ---[ 635]---> BDD-cost:   74
c ---[ 633]---> BDD-cost:   74
c ---[ 631]---> BDD-cost:   74
c ---[ 629]---> BDD-cost:   74
c ---[ 627]---> BDD-cost:   74
c ---[ 625]---> BDD-cost:   74
c ---[ 623]---> BDD-cost:   74
c ---[ 621]---> BDD-cost:   76
c ---[ 619]---> BDD-cost:   74
c ---[ 617]---> BDD-cost:   74
c ---[ 615]---> BDD-cost:   74
c ---[ 613]---> BDD-cost:   74
c ---[ 611]---> BDD-cost:   74
c ---[ 609]---> BDD-cost:   74
c ---[ 607]---> BDD-cost:   74
c ---[ 605]---> BDD-cost:   74
c ---[ 603]---> BDD-cost:   74
c ---[ 601]---> BDD-cost:   76
c ---[ 599]---> BDD-cost:   74
c ---[ 597]---> BDD-cost:   74
c ---[ 595]---> BDD-cost:   74
c ---[ 593]---> BDD-cost:   74
c ---[ 591]---> BDD-cost:   74
c ---[ 589]---> BDD-cost:   74
c ---[ 587]---> BDD-cost:   74
c ---[ 585]---> BDD-cost:   74
c ---[ 583]---> BDD-cost:   74
c ---[ 581]---> BDD-cost:   76
c ---[ 579]---> BDD-cost:   74
c ---[ 577]---> BDD-cost:   74
c ---[ 575]---> BDD-cost:   74
c ---[ 573]---> BDD-cost:   74
c ---[ 571]---> BDD-cost:   74
c ---[ 569]---> BDD-cost:   74
c ---[ 567]---> BDD-cost:   74
c ---[ 565]---> BDD-cost:   74
c ---[ 563]---> BDD-cost:   74
c ---[ 561]---> BDD-cost:   76
c ---[ 559]---> BDD-cost:   74
c ---[ 557]---> BDD-cost:   74
c ---[ 555]---> BDD-cost:   74
c ---[ 553]---> BDD-cost:   74
c ---[ 551]---> BDD-cost:   74
c ---[ 549]---> BDD-cost:   74
c ---[ 547]---> BDD-cost:   74
c ---[ 545]---> BDD-cost:   74
c ---[ 543]---> BDD-cost:   74
c ---[ 541]---> BDD-cost:   76
c ---[ 539]---> BDD-cost:   74
c ---[ 537]---> BDD-cost:   74
c ---[ 535]---> BDD-cost:   74
c ---[ 533]---> BDD-cost:   74
c ---[ 531]---> BDD-cost:   74
c ---[ 529]---> BDD-cost:   74
c ---[ 527]---> BDD-cost:   74
c ---[ 525]---> BDD-cost:   74
c ---[ 523]---> BDD-cost:   74
c ---[ 521]---> BDD-cost:   76
c ---[ 519]---> BDD-cost:   74
c ---[ 517]---> BDD-cost:   74
c ---[ 515]---> BDD-cost:   74
c ---[ 513]---> BDD-cost:   74
c ---[ 511]---> BDD-cost:   74
c ---[ 509]---> BDD-cost:   74
c ---[ 507]---> BDD-cost:   74
c ---[ 505]---> BDD-cost:   74
c ---[ 503]---> BDD-cost:   74
c ---[ 501]---> BDD-cost:   76
c ---[ 499]---> BDD-cost:   74
c ---[ 497]---> BDD-cost:   74
c ---[ 495]---> BDD-cost:   74
c ---[ 493]---> BDD-cost:   74
c ---[ 491]---> BDD-cost:   74
c ---[ 489]---> BDD-cost:   74
c ---[ 487]---> BDD-cost:   74
c ---[ 485]---> BDD-cost:   74
c ---[ 483]---> BDD-cost:   74
c ---[ 481]---> BDD-cost:   76
c ---[ 479]---> BDD-cost:   74
c ---[ 477]---> BDD-cost:   74
c ---[ 475]---> BDD-cost:   74
c ---[ 473]---> BDD-cost:   74
c ---[ 471]---> BDD-cost:   74
c ---[ 469]---> BDD-cost:   74
c ---[ 467]---> BDD-cost:   74
c ---[ 465]---> BDD-cost:   74
c ---[ 463]---> BDD-cost:   74
c ---[ 461]---> BDD-cost:   76
c ---[ 459]---> BDD-cost:   74
c ---[ 457]---> BDD-cost:   74
c ---[ 455]---> BDD-cost:   74
c ---[ 453]---> BDD-cost:   74
c ---[ 451]---> BDD-cost:   74
c ---[ 449]---> BDD-cost:   74
c ---[ 447]---> BDD-cost:   74
c ---[ 445]---> BDD-cost:   74
c ---[ 443]---> BDD-cost:   74
c ---[ 441]---> BDD-cost:   76
c ---[ 439]---> BDD-cost:   74
c ---[ 437]---> BDD-cost:   74
c ---[ 435]---> BDD-cost:   74
c ---[ 433]---> BDD-cost:   74
c ---[ 431]---> BDD-cost:   74
c ---[ 429]---> BDD-cost:   74
c ---[ 427]---> BDD-cost:   74
c ---[ 425]---> BDD-cost:   74
c ---[ 423]---> BDD-cost:   74
c ---[ 421]---> BDD-cost:   76
c ---[ 419]---> BDD-cost:   74
c ---[ 417]---> BDD-cost:   74
c ---[ 415]---> BDD-cost:   74
c ---[ 413]---> BDD-cost:   74
c ---[ 411]---> BDD-cost:   74
c ---[ 409]---> BDD-cost:   74
c ---[ 407]---> BDD-cost:   74
c ---[ 405]---> BDD-cost:   74
c ---[ 403]---> BDD-cost:   74
c ---[ 401]---> BDD-cost:   76
c ---[ 399]---> BDD-cost:   74
c ---[ 397]---> BDD-cost:   74
c ---[ 395]---> BDD-cost:   74
c ---[ 393]---> BDD-cost:   74
c ---[ 391]---> BDD-cost:   74
c ---[ 389]---> BDD-cost:   74
c ---[ 387]---> BDD-cost:   74
c ---[ 385]---> BDD-cost:   74
c ---[ 383]---> BDD-cost:   76
c ---[ 381]---> BDD-cost:   76
c ---[ 379]---> BDD-cost:   76
c ---[ 377]---> BDD-cost:   76
c ---[ 375]---> BDD-cost:   76
c ---[ 373]---> BDD-cost:   76
c ---[ 371]---> BDD-cost:   76
c ---[ 369]---> BDD-cost:   76
c ---[ 367]---> BDD-cost:   76
c ---[ 365]---> BDD-cost:   76
c ---[ 363]---> BDD-cost:   76
c ---[ 361]---> BDD-cost:   76
c ---[ 359]---> BDD-cost:   76
c ---[ 357]---> BDD-cost:   76
c ---[ 355]---> BDD-cost:   76
c ---[ 353]---> BDD-cost:   76
c ---[ 351]---> BDD-cost:   76
c ---[ 349]---> BDD-cost:   76
c ---[ 347]---> BDD-cost:   76
c ---[ 345]---> BDD-cost:   76
c ---[ 343]---> BDD-cost:   76
c ---[ 341]---> BDD-cost:   76
c ---[ 339]---> BDD-cost:   76
c ---[ 337]---> BDD-cost:   76
c ---[ 335]---> BDD-cost:   76
c ---[ 333]---> BDD-cost:   76
c ---[ 331]---> BDD-cost:   76
c ---[ 329]---> BDD-cost:   76
c ---[ 327]---> BDD-cost:   76
c ---[ 325]---> BDD-cost:   76
c ---[ 323]---> BDD-cost:   76
c ---[ 321]---> BDD-cost:   76
c ---[ 319]---> BDD-cost:   76
c ---[ 317]---> BDD-cost:   76
c ---[ 315]---> BDD-cost:   76
c ---[ 313]---> BDD-cost:   76
c ---[ 311]---> BDD-cost:   76
c ---[ 309]---> BDD-cost:   76
c ---[ 307]---> BDD-cost:   76
c ---[ 305]---> BDD-cost:   76
c ---[ 303]---> BDD-cost:   76
c ---[ 301]---> BDD-cost:   76
c ---[ 299]---> BDD-cost:   76
c ---[ 297]---> BDD-cost:   76
c ---[ 295]---> BDD-cost:   76
c ---[ 293]---> BDD-cost:   76
c ---[ 291]---> BDD-cost:   76
c ---[ 289]---> BDD-cost:   76
c ---[ 287]---> BDD-cost:   76
c ---[ 285]---> BDD-cost:   76
c ---[ 283]---> BDD-cost:   76
c ---[ 281]---> BDD-cost:   76
c ---[ 279]---> BDD-cost:   76
c ---[ 277]---> BDD-cost:   76
c ---[ 275]---> BDD-cost:   76
c ---[ 273]---> BDD-cost:   76
c ---[ 271]---> BDD-cost:   76
c ---[ 269]---> BDD-cost:   76
c ---[ 267]---> BDD-cost:   76
c ---[ 265]---> BDD-cost:   76
c ---[ 263]---> BDD-cost:   76
c ---[ 261]---> BDD-cost:   76
c ---[ 259]---> BDD-cost:   76
c ---[ 257]---> BDD-cost:   76
c ---[ 255]---> BDD-cost:   76
c ---[ 253]---> BDD-cost:   76
c ---[ 251]---> BDD-cost:   76
c ---[ 249]---> BDD-cost:   76
c ---[ 247]---> BDD-cost:   76
c ---[ 245]---> BDD-cost:   76
c ---[ 243]---> BDD-cost:   76
c ---[ 241]---> BDD-cost:   76
c ---[ 239]---> BDD-cost:   76
c ---[ 237]---> BDD-cost:   76
c ---[ 235]---> BDD-cost:   76
c ---[ 233]---> BDD-cost:   76
c ---[ 231]---> BDD-cost:   76
c ---[ 229]---> BDD-cost:   76
c ---[ 227]---> BDD-cost:   76
c ---[ 225]---> BDD-cost:   76
c ---[ 223]---> BDD-cost:   76
c ---[ 221]---> BDD-cost:   76
c ---[ 219]---> BDD-cost:   76
c ---[ 217]---> BDD-cost:   76
c ---[ 215]---> BDD-cost:   76
c ---[ 213]---> BDD-cost:   76
c ---[ 211]---> BDD-cost:   76
c ---[ 209]---> BDD-cost:   76
c ---[ 207]---> BDD-cost:   76
c ---[ 205]---> BDD-cost:   76
c ---[ 203]---> BDD-cost:   76
c ---[ 201]---> BDD-cost:   76
c ---[ 199]---> BDD-cost:   76
c ---[ 197]---> BDD-cost:   76
c ---[ 195]---> BDD-cost:   76
c ---[ 193]---> BDD-cost:   76
c ---[ 191]---> BDD-cost:   76
c ---[ 189]---> BDD-cost:   76
c ---[ 187]---> BDD-cost:   76
c ---[ 185]---> BDD-cost:   76
c ---[ 183]---> BDD-cost:   76
c ---[ 181]---> BDD-cost:   76
c ---[ 179]---> BDD-cost:   76
c ---[ 177]---> BDD-cost:   76
c ---[ 175]---> BDD-cost:   76
c ---[ 173]---> BDD-cost:   76
c ---[ 171]---> BDD-cost:   76
c ---[ 169]---> BDD-cost:   76
c ---[ 167]---> BDD-cost:   76
c ---[ 165]---> BDD-cost:   76
c ---[ 163]---> BDD-cost:   76
c ---[ 161]---> BDD-cost:   76
c ---[ 159]---> BDD-cost:   76
c ---[ 157]---> BDD-cost:   76
c ---[ 155]---> BDD-cost:   76
c ---[ 153]---> BDD-cost:   76
c ---[ 151]---> BDD-cost:   76
c ---[ 149]---> BDD-cost:   76
c ---[ 147]---> BDD-cost:   76
c ---[ 145]---> BDD-cost:   76
c ---[ 144]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 143]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 142]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 141]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 140]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 139]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 138]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 137]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 136]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[ 135]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 134]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 133]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 132]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 131]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 130]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 129]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 128]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 127]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 126]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 125]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 124]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 123]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 122]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 121]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 120]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 119]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 118]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[ 117]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 115]---> Adder-cost: 974   maxlim: 4217009   bits: 24/23
c ---[ 114]---> Adder-cost: 972   maxlim: 4218289   bits: 24/23
c ---[ 113]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[ 112]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[ 111]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 110]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 109]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 108]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[ 107]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 106]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[ 105]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 104]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 103]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 102]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 101]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[ 100]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[  99]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[  98]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  96]---> Adder-cost: 974   maxlim: 4214449   bits: 24/23
c ---[  95]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  94]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  93]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  92]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  91]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  90]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  89]---> Adder-cost: 970   maxlim: 4213809   bits: 24/23
c ---[  88]---> Adder-cost: 714   maxlim: 3162809   bits: 23/22
c ---[  86]---> Adder-cost: 714   maxlim: 3164089   bits: 23/22
c ---[  85]---> Adder-cost: 674   maxlim: 3164729   bits: 23/22
c ---[  84]---> Adder-cost: 674   maxlim: 3165369   bits: 23/22
c ---[  83]---> Adder-cost: 674   maxlim: 3165369   bits: 23/22
c ---[  82]---> Adder-cost: 674   maxlim: 3165369   bits: 23/22
c ---[  81]---> Adder-cost: 674   maxlim: 3164089   bits: 23/22
c ---[  80]---> Adder-cost: 674   maxlim: 3164089   bits: 23/22
c ---[  79]---> Adder-cost: 634   maxlim: 3162809   bits: 23/22
c ---[  78]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  76]---> Adder-cost: 974   maxlim: 4213809   bits: 24/23
c ---[  75]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  74]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  73]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  72]---> Adder-cost: 972   maxlim: 4215089   bits: 24/23
c ---[  71]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  70]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[  69]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[  68]---> Adder-cost: 714   maxlim: 3162809   bits: 23/22
c ---[  67]---> Adder-cost: 714   maxlim: 3163449   bits: 23/22
c ---[  66]---> Adder-cost: 674   maxlim: 3164089   bits: 23/22
c ---[  65]---> Adder-cost: 674   maxlim: 3165369   bits: 23/22
c ---[  64]---> Adder-cost: 674   maxlim: 3166649   bits: 23/22
c ---[  63]---> Adder-cost: 674   maxlim: 3164089   bits: 23/22
c ---[  62]---> Adder-cost: 674   maxlim: 3163449   bits: 23/22
c ---[  61]---> Adder-cost: 674   maxlim: 3162809   bits: 23/22
c ---[  60]---> Adder-cost: 634   maxlim: 3162809   bits: 23/22
c ---[  59]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[  58]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[  57]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  56]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  55]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  54]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  53]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  52]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  51]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[  50]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  49]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  48]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  47]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  46]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  45]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  44]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  43]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  42]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  41]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  40]---> Adder-cost: 974   maxlim: 4214449   bits: 24/23
c ---[  39]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  38]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  37]---> Adder-cost: 972   maxlim: 4219569   bits: 24/23
c ---[  36]---> Adder-cost: 972   maxlim: 4215729   bits: 24/23
c ---[  35]---> Adder-cost: 972   maxlim: 4217009   bits: 24/23
c ---[  34]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[  33]---> Adder-cost: 970   maxlim: 4213809   bits: 24/23
c ---[  32]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  31]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  30]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  29]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  28]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  27]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  26]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  25]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  24]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  23]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  22]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  21]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  20]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  19]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  18]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  17]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  16]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  15]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  14]---> Adder-cost: 974   maxlim: 4213169   bits: 24/23
c ---[  12]---> Adder-cost: 974   maxlim: 4213809   bits: 24/23
c ---[  11]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[  10]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   9]---> Adder-cost: 972   maxlim: 4214449   bits: 24/23
c ---[   8]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   7]---> Adder-cost: 972   maxlim: 4213809   bits: 24/23
c ---[   6]---> Adder-cost: 972   maxlim: 4213169   bits: 24/23
c ---[   5]---> Adder-cost: 970   maxlim: 4213169   bits: 24/23
c ---[   4]---> Adder-cost: 333   maxlim: 1279   bits: 12/11
c ---[   3]---> Adder-cost: 333   maxlim: 1279   bits: 12/11
c ---[   2]---> Adder-cost: 186   maxlim: 639   bits: 11/10
c ---[   1]---> Adder-cost: 287   maxlim: 639   bits: 11/10
c ---[   0]---> Adder-cost: 287   maxlim: 639   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2796853  7571342 |  932284       0        0     nan |  0.000 % |
c |       100 | 2796853  7571342 | 1025512     100      327     3.3 |  2.269 % |
c |       250 | 2796853  7571342 | 1128063     250      808     3.2 |  2.269 % |
c |       476 | 2796828  7571287 | 1240870     475     1726     3.6 |  2.270 % |
c |       813 | 2796748  7571109 | 1364957     808     3159     3.9 |  2.273 % |
c |      1319 | 2796748  7571109 | 1501452    1314     6308     4.8 |  2.273 % |
c |      2078 | 2796748  7571109 | 1651597    2073    10290     5.0 |  2.273 % |
c |      3217 | 2796748  7571109 | 1816757    3212    20707     6.4 |  2.273 % |
c |      4925 | 2796748  7571109 | 1998433    4920    30345     6.2 |  2.273 % |
c |      7487 | 2796668  7570933 | 2198276    7479    47382     6.3 |  2.276 % |
c |     11332 | 2796522  7570609 | 2418104   11321    78871     7.0 |  2.280 % |
c |     17098 | 2796401  7570341 | 2659915   17080   126914     7.4 |  2.284 % |
c |     25747 | 2796065  7569597 | 2925906   25711   199071     7.7 |  2.295 % |
c |     38721 | 2795299  7567905 | 3218497   38644   316646     8.2 |  2.321 % |
c |     58182 | 2794679  7566533 | 3540346   58077   603121    10.4 |  2.341 % |
c |     87375 | 2794679  7566533 | 3894381   87270  1614668    18.5 |  2.341 % |
c |    131164 | 2790706  7557713 | 4283819  130888  2399270    18.3 |  2.471 % |
c |    196848 | 2786421  7548184 | 4712201  196357  3105359    15.8 |  2.615 % |
#### 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.76 0.88 0.88 2/54 4820
Raw data (stat): 4820 (runsolver) R 4819 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 475798277 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0085 s]
Raw data (loadavg): 0.80 0.88 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 14813 0 0 0 965 34 0 0 25 0 1 0 475798277 54530048 11973 4294967295 134512640 134672761 3221224624 3221222400 134522987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13313 11973 603 41 0 13272 0
vsize: 53252
[startup+20.0094 s]
Raw data (loadavg): 0.83 0.88 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 47584 0 0 0 1891 109 0 0 25 0 1 0 475798277 223371264 44744 4294967295 134512640 134672761 3221224624 3221182724 134527673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54534 44744 603 41 0 54493 0
vsize: 218136
[startup+30.0107 s]
Raw data (loadavg): 0.85 0.89 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 71732 0 0 0 2835 164 0 0 25 0 1 0 475798277 309694464 68892 4294967295 134512640 134672761 3221224624 3221223792 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75609 68892 603 41 0 75568 0
vsize: 302436
[startup+40.0105 s]
Raw data (loadavg): 0.88 0.89 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 71931 0 0 0 3834 165 0 0 25 0 1 0 475798277 310370304 69091 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75774 69091 603 41 0 75733 0
vsize: 303096
[startup+50.0107 s]
Raw data (loadavg): 0.89 0.89 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 71981 0 0 0 4834 166 0 0 25 0 1 0 475798277 310640640 69141 4294967295 134512640 134672761 3221224624 3221223748 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75840 69141 603 41 0 75799 0
vsize: 303360
[startup+60.0109 s]
Raw data (loadavg): 0.91 0.90 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72098 0 0 0 5833 166 0 0 25 0 1 0 475798277 311046144 69258 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75939 69258 603 41 0 75898 0
vsize: 303756
[startup+70.0118 s]
Raw data (loadavg): 0.92 0.90 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72159 0 0 0 6833 167 0 0 25 0 1 0 475798277 311181312 69319 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75972 69319 603 41 0 75931 0
vsize: 303888
[startup+80.012 s]
Raw data (loadavg): 0.93 0.90 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72352 0 0 0 7832 168 0 0 25 0 1 0 475798277 311857152 69512 4294967295 134512640 134672761 3221224624 3221223748 134566151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76137 69512 603 41 0 76096 0
vsize: 304548
[startup+90.0123 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72436 0 0 0 8831 168 0 0 25 0 1 0 475798277 312221696 69596 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76226 69596 603 41 0 76185 0
vsize: 304904
[startup+100.013 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72482 0 0 0 9831 169 0 0 25 0 1 0 475798277 312356864 69642 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76259 69642 603 41 0 76218 0
vsize: 305036
[startup+110.013 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72569 0 0 0 10830 170 0 0 25 0 1 0 475798277 312762368 69729 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76358 69729 603 41 0 76317 0
vsize: 305432
[startup+120.015 s]
Raw data (loadavg): 0.97 0.91 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72684 0 0 0 11829 171 0 0 25 0 1 0 475798277 313167872 69844 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76457 69844 603 41 0 76416 0
vsize: 305828
[startup+130.015 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72759 0 0 0 12829 171 0 0 25 0 1 0 475798277 313438208 69919 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76523 69919 603 41 0 76482 0
vsize: 306092
[startup+140.015 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72800 0 0 0 13829 171 0 0 25 0 1 0 475798277 313573376 69960 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76556 69960 603 41 0 76515 0
vsize: 306224
[startup+150.019 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72864 0 0 0 14829 172 0 0 25 0 1 0 475798277 313708544 70024 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76589 70024 603 41 0 76548 0
vsize: 306356
[startup+160.019 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72901 0 0 0 15828 172 0 0 25 0 1 0 475798277 313843712 70061 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76622 70061 603 41 0 76581 0
vsize: 306488
[startup+170.019 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 72943 0 0 0 16828 173 0 0 25 0 1 0 475798277 313978880 70103 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76655 70103 603 41 0 76614 0
vsize: 306620
[startup+180.019 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73032 0 0 0 17827 173 0 0 25 0 1 0 475798277 314249216 70192 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76721 70192 603 41 0 76680 0
vsize: 306884
[startup+190.02 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73055 0 0 0 18827 174 0 0 25 0 1 0 475798277 314384384 70215 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76754 70215 603 41 0 76713 0
vsize: 307016
[startup+200.02 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73092 0 0 0 19827 174 0 0 25 0 1 0 475798277 314646528 70252 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76818 70252 603 41 0 76777 0
vsize: 307272
[startup+210.021 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73200 0 0 0 20826 174 0 0 25 0 1 0 475798277 315052032 70360 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76917 70360 603 41 0 76876 0
vsize: 307668
[startup+220.021 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73224 0 0 0 21826 175 0 0 25 0 1 0 475798277 315187200 70384 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76950 70384 603 41 0 76909 0
vsize: 307800
[startup+230.022 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73275 0 0 0 22826 175 0 0 25 0 1 0 475798277 315322368 70435 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76983 70435 603 41 0 76942 0
vsize: 307932
[startup+240.022 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73309 0 0 0 23826 175 0 0 25 0 1 0 475798277 315457536 70469 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77016 70469 603 41 0 76975 0
vsize: 308064
[startup+250.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73349 0 0 0 24825 176 0 0 25 0 1 0 475798277 315588608 70509 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77048 70509 603 41 0 77007 0
vsize: 308192
[startup+260.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73409 0 0 0 25825 176 0 0 25 0 1 0 475798277 315858944 70569 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77114 70569 603 41 0 77073 0
vsize: 308456
[startup+270.024 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73447 0 0 0 26824 177 0 0 25 0 1 0 475798277 315994112 70607 4294967295 134512640 134672761 3221224624 3221223776 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77147 70607 603 41 0 77106 0
vsize: 308588
[startup+280.025 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73477 0 0 0 27824 177 0 0 25 0 1 0 475798277 316129280 70637 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77180 70637 603 41 0 77139 0
vsize: 308720
[startup+290.025 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73518 0 0 0 28824 178 0 0 25 0 1 0 475798277 316264448 70678 4294967295 134512640 134672761 3221224624 3221223792 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77213 70678 603 41 0 77172 0
vsize: 308852
[startup+300.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73601 0 0 0 29823 178 0 0 25 0 1 0 475798277 316534784 70761 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77279 70761 603 41 0 77238 0
vsize: 309116
[startup+310.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 73941 0 0 0 30822 180 0 0 25 0 1 0 475798277 317882368 71101 4294967295 134512640 134672761 3221224624 3221223792 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77608 71101 603 41 0 77567 0
vsize: 310432
[startup+320.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 74139 0 0 0 31821 181 0 0 25 0 1 0 475798277 318951424 71299 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77869 71299 603 41 0 77828 0
vsize: 311476
[startup+330.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 74587 0 0 0 32818 183 0 0 25 0 1 0 475798277 320700416 71747 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78296 71747 603 41 0 78255 0
vsize: 313184
[startup+340.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 74914 0 0 0 33817 185 0 0 25 0 1 0 475798277 322048000 72074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78625 72074 603 41 0 78584 0
vsize: 314500
[startup+350.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 75287 0 0 0 34815 186 0 0 25 0 1 0 475798277 323534848 72447 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78988 72447 603 41 0 78947 0
vsize: 315952
[startup+360.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 75743 0 0 0 35814 188 0 0 25 0 1 0 475798277 325419008 72903 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79448 72903 603 41 0 79407 0
vsize: 317792
[startup+370.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 75784 0 0 0 36814 188 0 0 25 0 1 0 475798277 325554176 72944 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79481 72944 603 41 0 79440 0
vsize: 317924
[startup+380.029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 75811 0 0 0 37814 188 0 0 25 0 1 0 475798277 325689344 72971 4294967295 134512640 134672761 3221224624 3221223840 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79514 72971 603 41 0 79473 0
vsize: 318056
[startup+390.029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 75835 0 0 0 38814 188 0 0 25 0 1 0 475798277 325824512 72995 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79547 72995 603 41 0 79506 0
vsize: 318188
[startup+400.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 75861 0 0 0 39814 189 0 0 25 0 1 0 475798277 325824512 73021 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79547 73021 603 41 0 79506 0
vsize: 318188
[startup+410.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 75884 0 0 0 40814 189 0 0 25 0 1 0 475798277 325959680 73044 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79580 73044 603 41 0 79539 0
vsize: 318320
[startup+420.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 75966 0 0 0 41814 189 0 0 25 0 1 0 475798277 326225920 73126 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79645 73126 603 41 0 79604 0
vsize: 318580
[startup+430.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76012 0 0 0 42814 189 0 0 25 0 1 0 475798277 326496256 73172 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79711 73172 603 41 0 79670 0
vsize: 318844
[startup+440.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76047 0 0 0 43814 189 0 0 25 0 1 0 475798277 326631424 73207 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79744 73207 603 41 0 79703 0
vsize: 318976
[startup+450.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76079 0 0 0 44814 189 0 0 25 0 1 0 475798277 326766592 73239 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79777 73239 603 41 0 79736 0
vsize: 319108
[startup+460.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76103 0 0 0 45814 189 0 0 25 0 1 0 475798277 326766592 73263 4294967295 134512640 134672761 3221224624 3221223812 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79777 73263 603 41 0 79736 0
vsize: 319108
[startup+470.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76129 0 0 0 46815 189 0 0 25 0 1 0 475798277 326901760 73289 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79810 73289 603 41 0 79769 0
vsize: 319240
[startup+480.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76165 0 0 0 47815 189 0 0 25 0 1 0 475798277 327036928 73325 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79843 73325 603 41 0 79802 0
vsize: 319372
[startup+490.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76224 0 0 0 48815 190 0 0 25 0 1 0 475798277 327307264 73384 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79909 73384 603 41 0 79868 0
vsize: 319636
[startup+500.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76267 0 0 0 49815 190 0 0 25 0 1 0 475798277 327438336 73427 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79941 73427 603 41 0 79900 0
vsize: 319764
[startup+510.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76289 0 0 0 50815 190 0 0 25 0 1 0 475798277 327573504 73449 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79974 73449 603 41 0 79933 0
vsize: 319896
[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76320 0 0 0 51815 190 0 0 25 0 1 0 475798277 327708672 73480 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80007 73480 603 41 0 79966 0
vsize: 320028
[startup+530.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76347 0 0 0 52815 190 0 0 25 0 1 0 475798277 327843840 73507 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80040 73507 603 41 0 79999 0
vsize: 320160
[startup+540.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76367 0 0 0 53815 190 0 0 25 0 1 0 475798277 327843840 73527 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80040 73527 603 41 0 79999 0
vsize: 320160
[startup+550.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76399 0 0 0 54816 190 0 0 25 0 1 0 475798277 327979008 73559 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80073 73559 603 41 0 80032 0
vsize: 320292
[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76426 0 0 0 55816 190 0 0 25 0 1 0 475798277 328114176 73586 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80106 73586 603 41 0 80065 0
vsize: 320424
[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76452 0 0 0 56816 190 0 0 25 0 1 0 475798277 328249344 73612 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80139 73612 603 41 0 80098 0
vsize: 320556
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76468 0 0 0 57816 190 0 0 25 0 1 0 475798277 328249344 73628 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80139 73628 603 41 0 80098 0
vsize: 320556
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76473 0 0 0 58816 190 0 0 25 0 1 0 475798277 328249344 73633 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80139 73633 603 41 0 80098 0
vsize: 320556
[startup+600.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76496 0 0 0 59816 190 0 0 25 0 1 0 475798277 328384512 73656 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80172 73656 603 41 0 80131 0
vsize: 320688
[startup+610.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76520 0 0 0 60816 190 0 0 25 0 1 0 475798277 328519680 73680 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80205 73680 603 41 0 80164 0
vsize: 320820
[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76562 0 0 0 61817 190 0 0 25 0 1 0 475798277 328654848 73722 4294967295 134512640 134672761 3221224624 3221223776 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80238 73722 603 41 0 80197 0
vsize: 320952
[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76608 0 0 0 62816 191 0 0 25 0 1 0 475798277 329314304 73768 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80399 73768 603 41 0 80358 0
vsize: 321596
[startup+640.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76645 0 0 0 63815 191 0 0 25 0 1 0 475798277 329445376 73805 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80431 73805 603 41 0 80390 0
vsize: 321724
[startup+650.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76718 0 0 0 64815 191 0 0 25 0 1 0 475798277 329715712 73878 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80497 73878 603 41 0 80456 0
vsize: 321988
[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76753 0 0 0 65815 191 0 0 25 0 1 0 475798277 329850880 73913 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80530 73913 603 41 0 80489 0
vsize: 322120
[startup+670.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76767 0 0 0 66815 191 0 0 25 0 1 0 475798277 329986048 73927 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80563 73927 603 41 0 80522 0
vsize: 322252
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76787 0 0 0 67816 191 0 0 25 0 1 0 475798277 329986048 73947 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80563 73947 603 41 0 80522 0
vsize: 322252
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76836 0 0 0 68816 192 0 0 25 0 1 0 475798277 330252288 73996 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80628 73996 603 41 0 80587 0
vsize: 322512
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76879 0 0 0 69815 192 0 0 25 0 1 0 475798277 330387456 74039 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80661 74039 603 41 0 80620 0
vsize: 322644
[startup+710.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76953 0 0 0 70815 192 0 0 25 0 1 0 475798277 330657792 74113 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80727 74113 603 41 0 80686 0
vsize: 322908
[startup+720.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 76979 0 0 0 71826 192 0 0 25 0 1 0 475798277 330792960 74139 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80760 74139 603 41 0 80719 0
vsize: 323040
[startup+730.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77002 0 0 0 72826 192 0 0 25 0 1 0 475798277 330792960 74162 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80760 74162 603 41 0 80719 0
vsize: 323040
[startup+740.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77057 0 0 0 73826 193 0 0 25 0 1 0 475798277 331063296 74217 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80826 74217 603 41 0 80785 0
vsize: 323304
[startup+750.147 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77077 0 0 0 74827 193 0 0 25 0 1 0 475798277 331198464 74237 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80859 74237 603 41 0 80818 0
vsize: 323436
[startup+760.147 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77115 0 0 0 75826 193 0 0 25 0 1 0 475798277 331333632 74275 4294967295 134512640 134672761 3221224624 3221223776 134565132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80892 74275 603 41 0 80851 0
vsize: 323568
[startup+770.148 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77137 0 0 0 76826 193 0 0 25 0 1 0 475798277 331333632 74297 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80892 74297 603 41 0 80851 0
vsize: 323568
[startup+780.148 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77149 0 0 0 77826 194 0 0 25 0 1 0 475798277 331468800 74309 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80925 74309 603 41 0 80884 0
vsize: 323700
[startup+790.149 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77165 0 0 0 78826 194 0 0 25 0 1 0 475798277 331468800 74325 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80925 74325 603 41 0 80884 0
vsize: 323700
[startup+800.149 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77195 0 0 0 79826 194 0 0 25 0 1 0 475798277 331603968 74355 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80958 74355 603 41 0 80917 0
vsize: 323832
[startup+810.149 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77221 0 0 0 80827 194 0 0 25 0 1 0 475798277 331739136 74381 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80991 74381 603 41 0 80950 0
vsize: 323964
[startup+820.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77241 0 0 0 81827 194 0 0 25 0 1 0 475798277 331739136 74401 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80991 74401 603 41 0 80950 0
vsize: 323964
[startup+830.149 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77285 0 0 0 82827 194 0 0 25 0 1 0 475798277 332009472 74445 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81057 74445 603 41 0 81016 0
vsize: 324228
[startup+840.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77321 0 0 0 83827 194 0 0 25 0 1 0 475798277 332009472 74481 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81057 74481 603 41 0 81016 0
vsize: 324228
[startup+850.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77353 0 0 0 84827 194 0 0 25 0 1 0 475798277 332144640 74513 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81090 74513 603 41 0 81049 0
vsize: 324360
[startup+860.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77369 0 0 0 85827 194 0 0 25 0 1 0 475798277 332279808 74529 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81123 74529 603 41 0 81082 0
vsize: 324492
[startup+870.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77389 0 0 0 86827 194 0 0 25 0 1 0 475798277 332279808 74549 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81123 74549 603 41 0 81082 0
vsize: 324492
[startup+880.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77395 0 0 0 87827 194 0 0 25 0 1 0 475798277 332414976 74555 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81156 74555 603 41 0 81115 0
vsize: 324624
[startup+890.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77422 0 0 0 88827 195 0 0 25 0 1 0 475798277 332414976 74582 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81156 74582 603 41 0 81115 0
vsize: 324624
[startup+900.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77458 0 0 0 89827 195 0 0 25 0 1 0 475798277 332550144 74618 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81189 74618 603 41 0 81148 0
vsize: 324756
[startup+910.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77484 0 0 0 90827 195 0 0 25 0 1 0 475798277 332685312 74644 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81222 74644 603 41 0 81181 0
vsize: 324888
[startup+920.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77519 0 0 0 91827 195 0 0 25 0 1 0 475798277 332820480 74679 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81255 74679 603 41 0 81214 0
vsize: 325020
[startup+930.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77539 0 0 0 92827 196 0 0 25 0 1 0 475798277 332955648 74699 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81288 74699 603 41 0 81247 0
vsize: 325152
[startup+940.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77565 0 0 0 93827 196 0 0 25 0 1 0 475798277 333090816 74725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81321 74725 603 41 0 81280 0
vsize: 325284
[startup+950.154 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77601 0 0 0 94827 196 0 0 25 0 1 0 475798277 333090816 74761 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81321 74761 603 41 0 81280 0
vsize: 325284
[startup+960.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77622 0 0 0 95828 196 0 0 25 0 1 0 475798277 333225984 74782 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81354 74782 603 41 0 81313 0
vsize: 325416
[startup+970.156 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77652 0 0 0 96828 196 0 0 25 0 1 0 475798277 333361152 74812 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81387 74812 603 41 0 81346 0
vsize: 325548
[startup+980.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77699 0 0 0 97828 196 0 0 25 0 1 0 475798277 333496320 74859 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81420 74859 603 41 0 81379 0
vsize: 325680
[startup+990.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77733 0 0 0 98828 196 0 0 25 0 1 0 475798277 333631488 74893 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81453 74893 603 41 0 81412 0
vsize: 325812
[startup+1000.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77754 0 0 0 99828 196 0 0 25 0 1 0 475798277 333631488 74914 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81453 74914 603 41 0 81412 0
vsize: 325812
[startup+1010.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77779 0 0 0 100828 196 0 0 25 0 1 0 475798277 333766656 74939 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81486 74939 603 41 0 81445 0
vsize: 325944
[startup+1020.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77830 0 0 0 101828 197 0 0 25 0 1 0 475798277 334036992 74990 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81552 74990 603 41 0 81511 0
vsize: 326208
[startup+1030.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77863 0 0 0 102828 197 0 0 25 0 1 0 475798277 334172160 75023 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81585 75023 603 41 0 81544 0
vsize: 326340
[startup+1040.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77895 0 0 0 103828 197 0 0 25 0 1 0 475798277 334172160 75055 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81585 75055 603 41 0 81544 0
vsize: 326340
[startup+1050.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77914 0 0 0 104829 197 0 0 25 0 1 0 475798277 334303232 75074 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81617 75074 603 41 0 81576 0
vsize: 326468
[startup+1060.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77946 0 0 0 105828 197 0 0 25 0 1 0 475798277 334438400 75106 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81650 75106 603 41 0 81609 0
vsize: 326600
[startup+1070.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77970 0 0 0 106828 197 0 0 25 0 1 0 475798277 334573568 75130 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81683 75130 603 41 0 81642 0
vsize: 326732
[startup+1080.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 77988 0 0 0 107829 197 0 0 25 0 1 0 475798277 334573568 75148 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81683 75148 603 41 0 81642 0
vsize: 326732
[startup+1090.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78016 0 0 0 108829 198 0 0 25 0 1 0 475798277 334708736 75176 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81716 75176 603 41 0 81675 0
vsize: 326864
[startup+1100.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78031 0 0 0 109829 198 0 0 25 0 1 0 475798277 334708736 75191 4294967295 134512640 134672761 3221224624 3221223776 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81716 75191 603 41 0 81675 0
vsize: 326864
[startup+1110.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78064 0 0 0 110829 198 0 0 25 0 1 0 475798277 334843904 75224 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81749 75224 603 41 0 81708 0
vsize: 326996
[startup+1120.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78081 0 0 0 111829 198 0 0 25 0 1 0 475798277 334979072 75241 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81782 75241 603 41 0 81741 0
vsize: 327128
[startup+1130.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78105 0 0 0 112828 198 0 0 25 0 1 0 475798277 334979072 75265 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81782 75265 603 41 0 81741 0
vsize: 327128
[startup+1140.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78119 0 0 0 113829 198 0 0 25 0 1 0 475798277 335114240 75279 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81815 75279 603 41 0 81774 0
vsize: 327260
[startup+1150.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78144 0 0 0 114829 199 0 0 25 0 1 0 475798277 335245312 75304 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81847 75304 603 41 0 81806 0
vsize: 327388
[startup+1160.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78157 0 0 0 115829 199 0 0 25 0 1 0 475798277 335245312 75317 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81847 75317 603 41 0 81806 0
vsize: 327388
[startup+1170.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78413 0 0 0 116829 199 0 0 25 0 1 0 475798277 336314368 75573 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82108 75573 603 41 0 82067 0
vsize: 328432
[startup+1180.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78441 0 0 0 117828 200 0 0 25 0 1 0 475798277 336314368 75601 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82108 75601 603 41 0 82067 0
vsize: 328432
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78482 0 0 0 118828 200 0 0 25 0 1 0 475798277 336584704 75642 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82174 75642 603 41 0 82133 0
vsize: 328696
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4820
Raw data (stat): 4820 (minisat+) R 4819 26667 26666 0 -1 0 78500 0 0 0 119829 200 0 0 25 0 1 0 475798277 336584704 75660 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82174 75660 603 41 0 82133 0
vsize: 328696
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.32 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4820
Raw data (stat): 4820 (minisat+) Z 4819 26667 26666 0 -1 12 78502 0 0 0 119829 215 0 0 25 0 1 0 475798277 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.32
CPU time (s): 1200.45
CPU user time (s): 1198.29
CPU system time (s): 2.15667
CPU usage (%): 100.011
Max. virtual memory (Kb): 328696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####