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-fit1p.opb
MD5SUM	466386fc28c4adb9c70eb7384ea57208
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	20520
Biggest coefficient in the objective function	1572864
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	1553988150
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	58038681600
Number of bits of the biggest number in a constraint	36
Biggest sum of numbers in a constraint	204926279575
Number of bits of the biggest sum of numbers	38
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.268958
Number of variables	31508
Total number of constraints	1026
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	1026
Minimum length of a constraint	14
Maximum length of a constraint	416
Trace number 31035

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-25 21:27:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22399 boxname=wulflinc10 idbench=1215 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  466386fc28c4adb9c70eb7384ea57208  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-fit1p.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-fit1p.opb
IDLAUNCH: 22399
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        562184 kB
Buffers:         35604 kB
Cached:         414192 kB
SwapCached:         92 kB
Active:          71340 kB
Inactive:       381164 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        561932 kB
SwapTotal:     2097136 kB
SwapFree:      2096752 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6392 kB
Slab:            14300 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:48:00 (client local time) WITH STATUS 152 IN 1229.97 SECONDS
stats: 22399 7 1229.97 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1653 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1714]---> BDD-cost:   15
c ---[1713]---> BDD-cost:   14
c ---[1712]---> BDD-cost:   14
c ---[1710]---> BDD-cost:   14
c ---[1709]---> BDD-cost:   15
c ---[1708]---> BDD-cost:   13
c ---[1707]---> BDD-cost:   13
c ---[1706]---> BDD-cost:   14
c ---[1705]---> BDD-cost:   14
c ---[1703]---> BDD-cost:   13
c ---[1702]---> BDD-cost:   14
c ---[1701]---> BDD-cost:   14
c ---[1700]---> BDD-cost:   13
c ---[1699]---> BDD-cost:   13
c ---[1698]---> BDD-cost:   14
c ---[1697]---> BDD-cost:   14
c ---[1695]---> BDD-cost:   13
c ---[1694]---> BDD-cost:   13
c ---[1693]---> BDD-cost:   15
c ---[1691]---> BDD-cost:   13
c ---[1690]---> BDD-cost:   15
c ---[1689]---> BDD-cost:   15
c ---[1688]---> BDD-cost:   14
c ---[1687]---> BDD-cost:   14
c ---[1686]---> BDD-cost:   13
c ---[1685]---> BDD-cost:   15
c ---[1683]---> BDD-cost:   14
c ---[1681]---> BDD-cost:   15
c ---[1680]---> BDD-cost:   14
c ---[1679]---> BDD-cost:   14
c ---[1678]---> BDD-cost:   15
c ---[1677]---> BDD-cost:   13
c ---[1676]---> BDD-cost:   13
c ---[1674]---> BDD-cost:   15
c ---[1673]---> BDD-cost:   13
c ---[1672]---> BDD-cost:   14
c ---[1671]---> BDD-cost:   14
c ---[1670]---> BDD-cost:   13
c ---[1669]---> BDD-cost:   15
c ---[1667]---> BDD-cost:   15
c ---[1666]---> BDD-cost:   14
c ---[1665]---> BDD-cost:   13
c ---[1664]---> BDD-cost:   16
c ---[1663]---> BDD-cost:   16
c ---[1662]---> BDD-cost:   13
c ---[1661]---> BDD-cost:   13
c ---[1660]---> BDD-cost:   15
c ---[1659]---> BDD-cost:   14
c ---[1658]---> BDD-cost:   14
c ---[1657]---> BDD-cost:   13
c ---[1656]---> BDD-cost:   14
c ---[1655]---> BDD-cost:   15
c ---[1652]---> BDD-cost:   13
c ---[1651]---> BDD-cost:   13
c ---[1650]---> BDD-cost:   15
c ---[1649]---> BDD-cost:   13
c ---[1648]---> BDD-cost:   13
c ---[1647]---> BDD-cost:   13
c ---[1646]---> BDD-cost:   15
c ---[1645]---> BDD-cost:   15
c ---[1644]---> BDD-cost:   15
c ---[1641]---> BDD-cost:   13
c ---[1639]---> BDD-cost:   13
c ---[1638]---> BDD-cost:   13
c ---[1636]---> BDD-cost:   14
c ---[1633]---> BDD-cost:   15
c ---[1632]---> BDD-cost:   13
c ---[1631]---> BDD-cost:   13
c ---[1630]---> BDD-cost:   14
c ---[1629]---> BDD-cost:   15
c ---[1628]---> BDD-cost:   14
c ---[1627]---> BDD-cost:   13
c ---[1626]---> BDD-cost:   13
c ---[1625]---> BDD-cost:   15
c ---[1624]---> BDD-cost:   14
c ---[1623]---> BDD-cost:   14
c ---[1622]---> BDD-cost:   15
c ---[1621]---> BDD-cost:   15
c ---[1620]---> BDD-cost:   15
c ---[1619]---> BDD-cost:   13
c ---[1617]---> BDD-cost:   13
c ---[1616]---> BDD-cost:   15
c ---[1615]---> BDD-cost:   13
c ---[1614]---> BDD-cost:   13
c ---[1613]---> BDD-cost:   14
c ---[1612]---> BDD-cost:   14
c ---[1611]---> BDD-cost:   15
c ---[1610]---> BDD-cost:   13
c ---[1609]---> BDD-cost:   15
c ---[1608]---> BDD-cost:   15
c ---[1606]---> BDD-cost:   14
c ---[1605]---> BDD-cost:   15
c ---[1604]---> BDD-cost:   13
c ---[1602]---> BDD-cost:   14
c ---[1601]---> BDD-cost:   15
c ---[1600]---> BDD-cost:   15
c ---[1599]---> BDD-cost:   14
c ---[1597]---> BDD-cost:   15
c ---[1596]---> BDD-cost:   14
c ---[1595]---> BDD-cost:   15
c ---[1594]---> BDD-cost:   14
c ---[1593]---> BDD-cost:   14
c ---[1592]---> BDD-cost:   14
c ---[1590]---> BDD-cost:   13
c ---[1589]---> BDD-cost:   13
c ---[1588]---> BDD-cost:   13
c ---[1587]---> BDD-cost:   13
c ---[1586]---> BDD-cost:   13
c ---[1585]---> BDD-cost:   14
c ---[1584]---> BDD-cost:   15
c ---[1583]---> BDD-cost:   13
c ---[1582]---> BDD-cost:   13
c ---[1581]---> BDD-cost:   13
c ---[1580]---> BDD-cost:   13
c ---[1579]---> BDD-cost:   14
c ---[1577]---> BDD-cost:   13
c ---[1575]---> BDD-cost:   15
c ---[1572]---> BDD-cost:   15
c ---[1571]---> BDD-cost:   15
c ---[1570]---> BDD-cost:   13
c ---[1569]---> BDD-cost:   14
c ---[1568]---> BDD-cost:   14
c ---[1567]---> BDD-cost:   15
c ---[1566]---> BDD-cost:   13
c ---[1564]---> BDD-cost:   13
c ---[1563]---> BDD-cost:   13
c ---[1562]---> BDD-cost:   14
c ---[1559]---> BDD-cost:   14
c ---[1558]---> BDD-cost:   14
c ---[1557]---> BDD-cost:   14
c ---[1555]---> BDD-cost:   14
c ---[1554]---> BDD-cost:   13
c ---[1553]---> BDD-cost:   16
c ---[1552]---> BDD-cost:   13
c ---[1551]---> BDD-cost:   13
c ---[1550]---> BDD-cost:   13
c ---[1549]---> BDD-cost:   15
c ---[1548]---> BDD-cost:   14
c ---[1546]---> BDD-cost:   14
c ---[1545]---> BDD-cost:   15
c ---[1544]---> BDD-cost:   13
c ---[1543]---> BDD-cost:   14
c ---[1542]---> BDD-cost:   14
c ---[1541]---> BDD-cost:   14
c ---[1539]---> BDD-cost:   13
c ---[1538]---> BDD-cost:   13
c ---[1537]---> BDD-cost:   13
c ---[1536]---> BDD-cost:   14
c ---[1534]---> BDD-cost:   14
c ---[1533]---> BDD-cost:   13
c ---[1532]---> BDD-cost:   14
c ---[1531]---> BDD-cost:   14
c ---[1530]---> BDD-cost:   13
c ---[1529]---> BDD-cost:   13
c ---[1528]---> BDD-cost:   13
c ---[1527]---> BDD-cost:   15
c ---[1526]---> BDD-cost:   15
c ---[1525]---> BDD-cost:   14
c ---[1524]---> BDD-cost:   14
c ---[1523]---> BDD-cost:   14
c ---[1522]---> BDD-cost:   13
c ---[1521]---> BDD-cost:   13
c ---[1520]---> BDD-cost:   15
c ---[1519]---> BDD-cost:   14
c ---[1518]---> BDD-cost:   13
c ---[1517]---> BDD-cost:   13
c ---[1514]---> BDD-cost:   14
c ---[1513]---> BDD-cost:   15
c ---[1511]---> BDD-cost:   13
c ---[1510]---> BDD-cost:   15
c ---[1509]---> BDD-cost:   13
c ---[1508]---> BDD-cost:   13
c ---[1507]---> BDD-cost:   13
c ---[1506]---> BDD-cost:   13
c ---[1505]---> BDD-cost:   13
c ---[1504]---> BDD-cost:   14
c ---[1503]---> BDD-cost:   14
c ---[1502]---> BDD-cost:   15
c ---[1501]---> BDD-cost:   15
c ---[1500]---> BDD-cost:   14
c ---[1498]---> BDD-cost:   15
c ---[1497]---> BDD-cost:   13
c ---[1493]---> BDD-cost:   14
c ---[1492]---> BDD-cost:   14
c ---[1491]---> BDD-cost:   14
c ---[1490]---> BDD-cost:   15
c ---[1489]---> BDD-cost:   15
c ---[1488]---> BDD-cost:   13
c ---[1487]---> BDD-cost:   13
c ---[1485]---> BDD-cost:   14
c ---[1484]---> BDD-cost:   13
c ---[1483]---> BDD-cost:   14
c ---[1482]---> BDD-cost:   13
c ---[1481]---> BDD-cost:   15
c ---[1480]---> BDD-cost:   14
c ---[1479]---> BDD-cost:   14
c ---[1478]---> BDD-cost:   14
c ---[1476]---> BDD-cost:   13
c ---[1475]---> BDD-cost:   15
c ---[1473]---> BDD-cost:   15
c ---[1472]---> BDD-cost:   15
c ---[1471]---> BDD-cost:   13
c ---[1470]---> BDD-cost:   14
c ---[1469]---> BDD-cost:   14
c ---[1468]---> BDD-cost:   14
c ---[1466]---> BDD-cost:   13
c ---[1465]---> BDD-cost:   14
c ---[1464]---> BDD-cost:   15
c ---[1463]---> BDD-cost:   13
c ---[1462]---> BDD-cost:   14
c ---[1461]---> BDD-cost:   15
c ---[1460]---> BDD-cost:   13
c ---[1459]---> BDD-cost:   14
c ---[1458]---> BDD-cost:   15
c ---[1456]---> BDD-cost:   16
c ---[1455]---> BDD-cost:   14
c ---[1454]---> BDD-cost:   13
c ---[1453]---> BDD-cost:   13
c ---[1451]---> BDD-cost:   15
c ---[1450]---> BDD-cost:   14
c ---[1448]---> BDD-cost:   13
c ---[1446]---> BDD-cost:   14
c ---[1444]---> BDD-cost:   14
c ---[1443]---> BDD-cost:   14
c ---[1442]---> BDD-cost:   15
c ---[1441]---> BDD-cost:   14
c ---[1440]---> BDD-cost:   13
c ---[1439]---> BDD-cost:   13
c ---[1438]---> BDD-cost:   13
c ---[1437]---> BDD-cost:   14
c ---[1436]---> BDD-cost:   13
c ---[1435]---> BDD-cost:   15
c ---[1434]---> BDD-cost:   13
c ---[1433]---> BDD-cost:   13
c ---[1432]---> BDD-cost:   13
c ---[1431]---> BDD-cost:   14
c ---[1429]---> BDD-cost:   15
c ---[1428]---> BDD-cost:   14
c ---[1427]---> BDD-cost:   14
c ---[1426]---> BDD-cost:   14
c ---[1425]---> BDD-cost:   14
c ---[1424]---> BDD-cost:   13
c ---[1423]---> BDD-cost:   14
c ---[1422]---> BDD-cost:   14
c ---[1421]---> BDD-cost:   14
c ---[1420]---> BDD-cost:   14
c ---[1419]---> BDD-cost:   14
c ---[1418]---> BDD-cost:   15
c ---[1417]---> BDD-cost:   13
c ---[1416]---> BDD-cost:   13
c ---[1415]---> BDD-cost:   15
c ---[1414]---> BDD-cost:   13
c ---[1413]---> BDD-cost:   15
c ---[1412]---> BDD-cost:   14
c ---[1411]---> BDD-cost:   13
c ---[1410]---> BDD-cost:   13
c ---[1409]---> BDD-cost:   15
c ---[1408]---> BDD-cost:   15
c ---[1406]---> BDD-cost:   13
c ---[1405]---> BDD-cost:   14
c ---[1404]---> BDD-cost:   14
c ---[1403]---> BDD-cost:   13
c ---[1402]---> BDD-cost:   15
c ---[1400]---> BDD-cost:   14
c ---[1398]---> BDD-cost:   13
c ---[1397]---> BDD-cost:   14
c ---[1396]---> BDD-cost:   15
c ---[1395]---> BDD-cost:   13
c ---[1394]---> BDD-cost:   14
c ---[1392]---> BDD-cost:   13
c ---[1391]---> BDD-cost:   15
c ---[1390]---> BDD-cost:   14
c ---[1389]---> BDD-cost:   15
c ---[1388]---> BDD-cost:   14
c ---[1387]---> BDD-cost:   15
c ---[1385]---> BDD-cost:   13
c ---[1383]---> BDD-cost:   15
c ---[1382]---> BDD-cost:   13
c ---[1381]---> BDD-cost:   13
c ---[1380]---> BDD-cost:   13
c ---[1377]---> BDD-cost:   14
c ---[1376]---> BDD-cost:   13
c ---[1375]---> BDD-cost:   14
c ---[1374]---> BDD-cost:   15
c ---[1373]---> BDD-cost:   13
c ---[1372]---> BDD-cost:   14
c ---[1371]---> BDD-cost:   16
c ---[1370]---> BDD-cost:   13
c ---[1368]---> BDD-cost:   13
c ---[1367]---> BDD-cost:   14
c ---[1366]---> BDD-cost:   13
c ---[1364]---> BDD-cost:   15
c ---[1363]---> BDD-cost:   15
c ---[1362]---> BDD-cost:   13
c ---[1361]---> BDD-cost:   14
c ---[1360]---> BDD-cost:   15
c ---[1359]---> BDD-cost:   15
c ---[1358]---> BDD-cost:   14
c ---[1357]---> BDD-cost:   16
c ---[1356]---> BDD-cost:   14
c ---[1355]---> BDD-cost:   15
c ---[1354]---> BDD-cost:   13
c ---[1353]---> BDD-cost:   14
c ---[1352]---> BDD-cost:   14
c ---[1350]---> BDD-cost:   15
c ---[1349]---> BDD-cost:   14
c ---[1348]---> BDD-cost:   13
c ---[1347]---> BDD-cost:   13
c ---[1346]---> BDD-cost:   14
c ---[1345]---> BDD-cost:   14
c ---[1344]---> BDD-cost:   14
c ---[1343]---> BDD-cost:   15
c ---[1342]---> BDD-cost:   13
c ---[1341]---> BDD-cost:   17
c ---[1340]---> BDD-cost:   14
c ---[1339]---> BDD-cost:   13
c ---[1337]---> BDD-cost:   13
c ---[1336]---> BDD-cost:   14
c ---[1335]---> BDD-cost:   13
c ---[1334]---> BDD-cost:   14
c ---[1333]---> BDD-cost:   13
c ---[1332]---> BDD-cost:   15
c ---[1331]---> BDD-cost:   14
c ---[1330]---> BDD-cost:   13
c ---[1329]---> BDD-cost:   13
c ---[1328]---> BDD-cost:   14
c ---[1327]---> BDD-cost:   13
c ---[1325]---> BDD-cost:   14
c ---[1324]---> BDD-cost:   13
c ---[1323]---> BDD-cost:   13
c ---[1322]---> BDD-cost:   15
c ---[1321]---> BDD-cost:   14
c ---[1320]---> BDD-cost:   14
c ---[1319]---> BDD-cost:   13
c ---[1318]---> BDD-cost:   14
c ---[1317]---> BDD-cost:   14
c ---[1315]---> Sorter-cost:14715     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1313]---> Sorter-cost:18418     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1311]---> Sorter-cost:15328     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1309]---> Adder-cost: 474   maxlim: 5010336   bits: 24/23
c ---[1307]---> Adder-cost: 1418   maxlim: 83939090   bits: 28/27
c ---[1305]---> Adder-cost: 522   maxlim: 5911281   bits: 24/23
c ---[1303]---> Sorter-cost:19611     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1301]---> Adder-cost: 744   maxlim: 9189328   bits: 24/24
c ---[1299]---> Sorter-cost:19206     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1297]---> Sorter-cost:19874     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1295]---> Sorter-cost:19540     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1293]---> Sorter-cost:14751     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1291]---> Sorter-cost:15525     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1289]---> Sorter-cost:20285     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1287]---> Sorter-cost:19975     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1285]---> Adder-cost: 512   maxlim: 7288903   bits: 24/23
c ---[1283]---> Adder-cost: 1367   maxlim: 140370820   bits: 28/28
c ---[1281]---> Adder-cost: 2130   maxlim: 323768400   bits: 30/29
c ---[1279]---> Adder-cost: 1590   maxlim: 47250815   bits: 27/26
c ---[1277]---> Adder-cost: 1448   maxlim: 158305020   bits: 29/28
c ---[1275]---> Sorter-cost:21017     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1273]---> Adder-cost: 510   maxlim: 6912054   bits: 24/23
c ---[1271]---> Adder-cost: 1482   maxlim: 48898480   bits: 27/26
c ---[1269]---> Sorter-cost:19235     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1267]---> Sorter-cost:17969     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1265]---> Adder-cost: 1312   maxlim: 207920160   bits: 29/28
c ---[1263]---> Sorter-cost:14874     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1261]---> Adder-cost: 1656   maxlim: 251559140   bits: 29/28
c ---[1259]---> Adder-cost: 438   maxlim: 8499817   bits: 24/24
c ---[1257]---> Sorter-cost:11919     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1255]---> Sorter-cost:16524     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1253]---> Adder-cost: 1430   maxlim: 131286560   bits: 28/27
c ---[1251]---> Adder-cost: 1274   maxlim: 76966160   bits: 27/27
c ---[1249]---> Adder-cost: 1474   maxlim: 46886720   bits: 27/26
c ---[1247]---> Adder-cost: 864   maxlim: 9168634   bits: 24/24
c ---[1245]---> Sorter-cost:16176     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1243]---> Adder-cost: 708   maxlim: 7205654   bits: 24/23
c ---[1241]---> Sorter-cost:20587     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1239]---> Sorter-cost:14577     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1237]---> Sorter-cost:16245     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1235]---> Sorter-cost:14388     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1233]---> Sorter-cost:20993     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1231]---> Adder-cost: 1362   maxlim: 112367180   bits: 28/27
c ---[1229]---> Sorter-cost:14651     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1227]---> Adder-cost: 1530   maxlim: 38115715   bits: 27/26
c ---[1225]---> Sorter-cost:12584     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> Adder-cost: 1530   maxlim: 86063400   bits: 28/27
c ---[1221]---> Sorter-cost:15609     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost:19598     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1217]---> Sorter-cost:15646     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1215]---> Sorter-cost:15280     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1213]---> Sorter-cost:20566     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1211]---> Sorter-cost:16723     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1209]---> Sorter-cost:15857     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1207]---> Adder-cost: 580   maxlim: 13268802   bits: 24/24
c ---[1205]---> Sorter-cost:13552     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1203]---> Adder-cost: 738   maxlim: 8057506   bits: 24/23
c ---[1201]---> Adder-cost: 1240   maxlim: 78510020   bits: 28/27
c ---[1199]---> Adder-cost: 1974   maxlim: 547025700   bits: 31/30
c ---[1197]---> Adder-cost: 582   maxlim: 4713535   bits: 24/23
c ---[1195]---> Sorter-cost:15706     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1193]---> Adder-cost: 1048   maxlim: 111291980   bits: 28/27
c ---[1191]---> Sorter-cost:15973     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1189]---> Sorter-cost:11624     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1187]---> Adder-cost: 404   maxlim: 6977193   bits: 24/23
c ---[1185]---> Sorter-cost:15109     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1183]---> Adder-cost: 426   maxlim: 7600156   bits: 24/23
c ---[1181]---> Sorter-cost:16336     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1179]---> Sorter-cost:15442     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1177]---> Sorter-cost:14605     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1175]---> Adder-cost: 1828   maxlim: 255759650   bits: 29/28
c ---[1173]---> Sorter-cost:17448     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1171]---> Adder-cost: 1726   maxlim: 209167150   bits: 29/28
c ---[1169]---> Sorter-cost:15783     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1167]---> Adder-cost: 642   maxlim: 9844609   bits: 24/24
c ---[1165]---> Adder-cost: 1608   maxlim: 129311730   bits: 28/27
c ---[1163]---> Adder-cost: 656   maxlim: 7501732   bits: 24/23
c ---[1161]---> Adder-cost: 908   maxlim: 43376224   bits: 27/26
c ---[1159]---> Adder-cost: 862   maxlim: 24433288   bits: 26/25
c ---[1157]---> Adder-cost: 1304   maxlim: 74169520   bits: 28/27
c ---[1155]---> Sorter-cost:17637     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1153]---> Adder-cost: 606   maxlim: 6220584   bits: 24/23
c ---[1151]---> Sorter-cost:17720     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1149]---> Adder-cost: 1226   maxlim: 47082420   bits: 27/26
c ---[1147]---> Adder-cost: 1724   maxlim: 294353375   bits: 30/29
c ---[1145]---> Sorter-cost:13564     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1143]---> Adder-cost: 1826   maxlim: 285337660   bits: 29/29
c ---[1141]---> Sorter-cost:14665     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1139]---> Sorter-cost:20008     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1137]---> Sorter-cost:15201     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost:20836     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1133]---> Adder-cost: 1320   maxlim: 185403220   bits: 29/28
c ---[1131]---> Adder-cost: 828   maxlim: 23710612   bits: 26/25
c ---[1129]---> Sorter-cost:16253     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1127]---> Sorter-cost:22350     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1125]---> Sorter-cost:16425     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1123]---> Sorter-cost:12434     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1121]---> Sorter-cost:10742     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1119]---> Sorter-cost:21555     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1117]---> Sorter-cost:14443     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1115]---> Sorter-cost:11069     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1113]---> Adder-cost: 598   maxlim: 8263687   bits: 24/23
c ---[1111]---> Sorter-cost:14303     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1109]---> Adder-cost: 1374   maxlim: 76307190   bits: 28/27
c ---[1107]---> Adder-cost: 1148   maxlim: 132524060   bits: 28/27
c ---[1105]---> Sorter-cost:19664     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1103]---> Sorter-cost:21647     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1101]---> Sorter-cost:15685     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1099]---> Sorter-cost:16204     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1097]---> Sorter-cost:15595     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1095]---> Sorter-cost:17150     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1093]---> Sorter-cost:10426     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1091]---> Adder-cost: 1768   maxlim: 81247815   bits: 27/27
c ---[1089]---> Adder-cost: 772   maxlim: 12202373   bits: 24/24
c ---[1087]---> Adder-cost: 522   maxlim: 7204395   bits: 24/23
c ---[1085]---> Sorter-cost:17102     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1083]---> Adder-cost: 346   maxlim: 7597084   bits: 24/23
c ---[1081]---> Sorter-cost:15083     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1079]---> Sorter-cost:12535     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1077]---> Sorter-cost:17326     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1075]---> Adder-cost: 884   maxlim: 37262720   bits: 26/26
c ---[1073]---> Adder-cost: 2066   maxlim: 854072400   bits: 31/30
c ---[1071]---> Sorter-cost:15111     Base: 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1069]---> Sorter-cost:11786     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1067]---> Adder-cost: 514   maxlim: 4815363   bits: 24/23
c ---[1065]---> Sorter-cost:12839     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1063]---> Adder-cost: 604   maxlim: 7157787   bits: 24/23
c ---[1061]---> Sorter-cost:21978     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1059]---> Adder-cost: 1152   maxlim: 275525920   bits: 29/29
c ---[1057]---> Sorter-cost:15137     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1055]---> Adder-cost: 1591   maxlim: 127380050   bits: 28/27
c ---[1053]---> Sorter-cost:21358     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1051]---> Sorter-cost:13014     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1049]---> Sorter-cost:11686     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1047]---> Sorter-cost:14540     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1045]---> Adder-cost: 662   maxlim: 8795920   bits: 24/24
c ---[1043]---> Sorter-cost:14810     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1041]---> Adder-cost: 600   maxlim: 10024167   bits: 24/24
c ---[1039]---> Adder-cost: 602   maxlim: 12367778   bits: 24/24
c ---[1037]---> Sorter-cost:15893     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1035]---> Sorter-cost:13096     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1033]---> Sorter-cost:14664     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1031]---> Sorter-cost:10115     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1029]---> Adder-cost: 1286   maxlim: 37712315   bits: 27/26
c ---[1027]---> Sorter-cost:15015     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1025]---> Adder-cost: 340   maxlim: 7600156   bits: 24/23
c ---[1023]---> Sorter-cost:13000     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1021]---> Adder-cost: 476   maxlim: 7302637   bits: 24/23
c ---[1019]---> Adder-cost: 630   maxlim: 5380477   bits: 24/23
c ---[1017]---> Sorter-cost:14088     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1015]---> Adder-cost: 600   maxlim: 5866535   bits: 24/23
c ---[1013]---> Adder-cost: 594   maxlim: 6792726   bits: 24/23
c ---[1011]---> Sorter-cost:23446     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1009]---> Adder-cost: 618   maxlim: 5981109   bits: 24/23
c ---[1007]---> Sorter-cost:12223     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1005]---> Adder-cost: 1200   maxlim: 140209990   bits: 28/28
c ---[1003]---> Sorter-cost:16415     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1001]---> Sorter-cost:22445     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 999]---> Sorter-cost:16794     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 997]---> Sorter-cost:21496     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 995]---> Adder-cost: 510   maxlim: 4444317   bits: 23/23
c ---[ 993]---> Sorter-cost:13232     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 991]---> Sorter-cost:16689     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 989]---> Adder-cost: 452   maxlim: 6551581   bits: 23/23
c ---[ 987]---> Sorter-cost:11552     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 985]---> Adder-cost: 630   maxlim: 8632259   bits: 24/24
c ---[ 983]---> Sorter-cost:16568     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 981]---> Sorter-cost:14516     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 979]---> Sorter-cost:19466     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 977]---> Sorter-cost:15432     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 975]---> Sorter-cost:16349     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 973]---> Adder-cost: 618   maxlim: 14480336   bits: 24/24
c ---[ 971]---> Sorter-cost:17119     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 969]---> Adder-cost: 1010   maxlim: 74168390   bits: 27/27
c ---[ 967]---> Adder-cost: 1788   maxlim: 1031662200   bits: 31/30
c ---[ 965]---> Sorter-cost:18669     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 963]---> Adder-cost: 582   maxlim: 7759389   bits: 24/23
c ---[ 961]---> Adder-cost: 560   maxlim: 10962290   bits: 24/24
c ---[ 959]---> Sorter-cost:16538     Base: 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 957]---> Adder-cost: 1110   maxlim: 195870020   bits: 28/28
c ---[ 955]---> Adder-cost: 1432   maxlim: 83814780   bits: 28/27
c ---[ 953]---> Adder-cost: 548   maxlim: 7745798   bits: 24/23
c ---[ 951]---> Sorter-cost:21680     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 949]---> Sorter-cost:15857     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 947]---> Sorter-cost:12792     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 945]---> Adder-cost: 1680   maxlim: 442619625   bits: 30/29
c ---[ 943]---> Sorter-cost:15749     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 941]---> Sorter-cost:16430     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 939]---> Sorter-cost:23337     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 937]---> Adder-cost: 1132   maxlim: 61838340   bits: 27/26
c ---[ 935]---> Sorter-cost:18570     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 933]---> Sorter-cost:15595     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 931]---> Sorter-cost:11804     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 929]---> Adder-cost: 652   maxlim: 10991511   bits: 24/24
c ---[ 927]---> Sorter-cost:14726     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 925]---> Sorter-cost:13482     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 923]---> Sorter-cost:12471     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 921]---> Adder-cost: 646   maxlim: 16283642   bits: 25/24
c ---[ 919]---> Adder-cost: 788   maxlim: 9648231   bits: 25/24
c ---[ 917]---> Sorter-cost:16275     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 915]---> Sorter-cost:13301     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 913]---> Adder-cost: 1108   maxlim: 121639020   bits: 28/27
c ---[ 911]---> Adder-cost: 1213   maxlim: 127375580   bits: 28/27
c ---[ 909]---> Adder-cost: 1202   maxlim: 31327455   bits: 26/25
c ---[ 907]---> Adder-cost: 620   maxlim: 4659101   bits: 24/23
c ---[ 905]---> Sorter-cost:16232     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 903]---> Sorter-cost:14634     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 901]---> Adder-cost: 626   maxlim: 8865496   bits: 24/24
c ---[ 899]---> Sorter-cost:14377     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 897]---> Adder-cost: 646   maxlim: 8103412   bits: 24/23
c ---[ 895]---> Adder-cost: 1686   maxlim: 662431950   bits: 31/30
c ---[ 893]---> Adder-cost: 648   maxlim: 8990898   bits: 24/24
c ---[ 891]---> Sorter-cost:17165     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 889]---> Sorter-cost:20453     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 887]---> Adder-cost: 1194   maxlim: 134188380   bits: 28/27
c ---[ 885]---> Sorter-cost:15487     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 883]---> Sorter-cost:11161     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 881]---> Sorter-cost:19695     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 879]---> Adder-cost: 598   maxlim: 8575027   bits: 24/24
c ---[ 877]---> Sorter-cost:11713     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 875]---> Sorter-cost:18964     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 873]---> Sorter-cost:18195     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 871]---> Sorter-cost:13389     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 869]---> Adder-cost: 552   maxlim: 8631134   bits: 24/24
c ---[ 867]---> Sorter-cost:13865     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 865]---> Sorter-cost:12953     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 863]---> Sorter-cost:20043     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 861]---> Sorter-cost:15407     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 859]---> Sorter-cost:10260     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 857]---> Sorter-cost:11642     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 855]---> Sorter-cost:11885     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 853]---> Adder-cost: 410   maxlim: 6912054   bits: 24/23
c ---[ 851]---> Sorter-cost:13532     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 849]---> Adder-cost: 632   maxlim: 11711990   bits: 24/24
c ---[ 847]---> Sorter-cost:19835     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 845]---> Adder-cost: 476   maxlim: 9040731   bits: 24/24
c ---[ 843]---> Sorter-cost:15336     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 841]---> Sorter-cost:13898     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 839]---> Sorter-cost:22701     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 837]---> Sorter-cost:10886     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 835]---> Sorter-cost:12436     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 833]---> Adder-cost: 680   maxlim: 9939599   bits: 24/24
c ---[ 831]---> Sorter-cost:14926     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 829]---> Adder-cost: 592   maxlim: 7894414   bits: 24/23
c ---[ 827]---> Adder-cost: 1313   maxlim: 107439320   bits: 28/27
c ---[ 825]---> Sorter-cost:18693     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 823]---> Sorter-cost:23219     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 821]---> Sorter-cost:15915     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 819]---> Adder-cost: 650   maxlim: 12596464   bits: 24/24
c ---[ 817]---> Sorter-cost:16768     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 815]---> Adder-cost: 1062   maxlim: 106756940   bits: 28/27
c ---[ 813]---> Sorter-cost:20134     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 811]---> Adder-cost: 1224   maxlim: 146098520   bits: 28/28
c ---[ 809]---> Sorter-cost:14521     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 807]---> Sorter-cost:22617     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 805]---> Adder-cost: 1166   maxlim: 33945635   bits: 26/26
c ---[ 803]---> Sorter-cost:23793     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 801]---> Sorter-cost:11912     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 799]---> Sorter-cost:16346     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 797]---> Adder-cost: 1470   maxlim: 227477240   bits: 29/28
c ---[ 795]---> Adder-cost: 734   maxlim: 11505975   bits: 24/24
c ---[ 793]---> Adder-cost: 378   maxlim: 5863095   bits: 24/23
c ---[ 791]---> Sorter-cost:11508     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 789]---> Adder-cost: 418   maxlim: 6219703   bits: 23/23
c ---[ 787]---> Adder-cost: 584   maxlim: 8878231   bits: 24/24
c ---[ 785]---> Sorter-cost:13081     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 783]---> Sorter-cost:14020     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Adder-cost: 592   maxlim: 9340552   bits: 24/24
c ---[ 779]---> Sorter-cost:15379     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 777]---> Sorter-cost:17482     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> Adder-cost: 1164   maxlim: 37668740   bits: 27/26
c ---[ 773]---> Adder-cost: 408   maxlim: 5992797   bits: 23/23
c ---[ 771]---> Adder-cost: 1330   maxlim: 78935040   bits: 28/27
c ---[ 769]---> Sorter-cost:15854     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 767]---> Sorter-cost:18093     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 765]---> Sorter-cost:21759     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 763]---> Adder-cost: 1494   maxlim: 359452825   bits: 29/29
c ---[ 761]---> Adder-cost: 1814   maxlim: 1084401900   bits: 31/31
c ---[ 759]---> Adder-cost: 1352   maxlim: 241413960   bits: 29/28
c ---[ 757]---> Sorter-cost:20532     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 755]---> Sorter-cost:15010     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 753]---> Sorter-cost:13857     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 751]---> Adder-cost: 608   maxlim: 10057674   bits: 24/24
c ---[ 749]---> Adder-cost: 570   maxlim: 11188154   bits: 24/24
c ---[ 747]---> Sorter-cost:14904     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 745]---> Adder-cost: 736   maxlim: 8008902   bits: 24/23
c ---[ 743]---> Adder-cost: 1860   maxlim: 1205776200   bits: 31/31
c ---[ 741]---> Sorter-cost:18349     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 739]---> Adder-cost: 1146   maxlim: 171962180   bits: 28/28
c ---[ 737]---> Sorter-cost:15862     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 735]---> Sorter-cost:13669     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 733]---> Sorter-cost:15341     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 731]---> Sorter-cost:20629     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 729]---> Adder-cost: 1042   maxlim: 46575600   bits: 27/26
c ---[ 727]---> Sorter-cost:17353     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 725]---> Sorter-cost:15390     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 723]---> Sorter-cost:13211     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 721]---> Sorter-cost:15793     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 719]---> Adder-cost: 562   maxlim: 6141981   bits: 24/23
c ---[ 717]---> Sorter-cost:22664     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 715]---> Adder-cost: 636   maxlim: 4368127   bits: 24/23
c ---[ 713]---> Sorter-cost:18663     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 711]---> Sorter-cost:14890     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 709]---> Sorter-cost:15933     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 707]---> Sorter-cost:16610     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 705]---> Sorter-cost:12859     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 703]---> Sorter-cost:12932     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 701]---> Sorter-cost:12612     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 699]---> Adder-cost: 1240   maxlim: 71864780   bits: 28/27
c ---[ 697]---> Sorter-cost:15055     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 695]---> Sorter-cost:14583     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 693]---> Sorter-cost:14137     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 691]---> Adder-cost: 1412   maxlim: 42137960   bits: 27/26
c ---[ 689]---> Sorter-cost:15583     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> Adder-cost: 1402   maxlim: 300916080   bits: 29/29
c ---[ 685]---> Adder-cost: 1192   maxlim: 35368780   bits: 26/26
c ---[ 683]---> Sorter-cost:12654     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 681]---> Adder-cost: 470   maxlim: 5699280   bits: 24/23
c ---[ 679]---> Adder-cost: 462   maxlim: 5894121   bits: 24/23
c ---[ 677]---> Sorter-cost:15044     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 675]---> Sorter-cost:21299     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 673]---> Sorter-cost:18716     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 671]---> Sorter-cost:14529     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 669]---> Adder-cost: 530   maxlim: 12858856   bits: 24/24
c ---[ 667]---> Sorter-cost:19395     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 665]---> Adder-cost: 774   maxlim: 38059524   bits: 27/26
c ---[ 663]---> Sorter-cost:21969     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 661]---> Adder-cost: 468   maxlim: 6669281   bits: 24/23
c ---[ 659]---> Sorter-cost:22021     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 657]---> Adder-cost: 554   maxlim: 8088196   bits: 24/23
c ---[ 655]---> Sorter-cost:17103     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Adder-cost: 568   maxlim: 5925058   bits: 24/23
c ---[ 651]---> Sorter-cost:13938     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost:14636     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Sorter-cost:16451     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 645]---> Adder-cost: 508   maxlim: 6952802   bits: 24/23
c ---[ 643]---> Sorter-cost:14839     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost:21518     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 639]---> Adder-cost: 1572   maxlim: 98629925   bits: 28/27
c ---[ 637]---> Sorter-cost:15301     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost:20375     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost:15158     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Sorter-cost:14147     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 629]---> Sorter-cost:15357     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost:20224     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 625]---> Sorter-cost:19905     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> Adder-cost: 644   maxlim: 11528673   bits: 24/24
c ---[ 621]---> Sorter-cost:14242     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 619]---> Sorter-cost:14624     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 617]---> Adder-cost: 1056   maxlim: 156259740   bits: 28/28
c ---[ 615]---> Adder-cost: 1832   maxlim: 707112450   bits: 31/30
c ---[ 613]---> Sorter-cost:21078     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:19844     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Adder-cost: 540   maxlim: 6117409   bits: 24/23
c ---[ 607]---> Adder-cost: 1694   maxlim: 550772150   bits: 31/30
c ---[ 605]---> Sorter-cost:16571     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 603]---> Adder-cost: 488   maxlim: 10381005   bits: 24/24
c ---[ 601]---> Sorter-cost:10588     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost:17255     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost:10942     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost:15619     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost:10773     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:14043     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost:19191     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Adder-cost: 1206   maxlim: 127362000   bits: 28/27
c ---[ 585]---> Adder-cost: 1676   maxlim: 807251500   bits: 31/30
c ---[ 583]---> Sorter-cost:13566     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 581]---> Sorter-cost:10605     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 579]---> Sorter-cost:15794     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 577]---> Adder-cost: 1252   maxlim: 99222680   bits: 28/27
c ---[ 575]---> Sorter-cost:16029     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost:14797     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 571]---> Adder-cost: 1402   maxlim: 253434920   bits: 29/28
c ---[ 569]---> Adder-cost: 680   maxlim: 10022178   bits: 25/24
c ---[ 567]---> Adder-cost: 2186   maxlim: 609654725   bits: 30/30
c ---[ 565]---> Sorter-cost:14714     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 563]---> Adder-cost: 530   maxlim: 14267708   bits: 24/24
c ---[ 561]---> Adder-cost: 622   maxlim: 6681824   bits: 24/23
c ---[ 559]---> Sorter-cost:18812     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 557]---> Sorter-cost:14191     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 555]---> Adder-cost: 548   maxlim: 6060048   bits: 24/23
c ---[ 553]---> Adder-cost: 1068   maxlim: 39141200   bits: 27/26
c ---[ 551]---> Adder-cost: 570   maxlim: 6719579   bits: 24/23
c ---[ 549]---> Sorter-cost:12549     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Adder-cost: 1952   maxlim: 569964000   bits: 30/30
c ---[ 545]---> Sorter-cost:13195     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 543]---> Adder-cost: 588   maxlim: 15250983   bits: 24/24
c ---[ 541]---> Sorter-cost:12148     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 539]---> Sorter-cost:19345     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> Adder-cost: 1142   maxlim: 193428560   bits: 29/28
c ---[ 535]---> Adder-cost: 488   maxlim: 6909749   bits: 24/23
c ---[ 533]---> Sorter-cost:13891     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 531]---> Sorter-cost:16016     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 529]---> Sorter-cost:19291     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 527]---> Sorter-cost:16957     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 525]---> Adder-cost: 1456   maxlim: 92041660   bits: 28/27
c ---[ 523]---> Adder-cost: 1776   maxlim: 465198700   bits: 30/29
c ---[ 521]---> Sorter-cost:22638     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 519]---> Adder-cost: 1694   maxlim: 380706625   bits: 30/29
c ---[ 517]---> Sorter-cost:15209     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost:16850     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 513]---> Adder-cost: 1806   maxlim: 425357125   bits: 30/29
c ---[ 511]---> Sorter-cost:15879     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 509]---> Sorter-cost:17918     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Sorter-cost:18711     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Adder-cost: 1291   maxlim: 24200915   bits: 26/25
c ---[ 503]---> Adder-cost: 1136   maxlim: 149395160   bits: 28/28
c ---[ 501]---> Sorter-cost:13910     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 499]---> Sorter-cost:14119     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost:15193     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Adder-cost: 1452   maxlim: 143908340   bits: 29/28
c ---[ 493]---> Adder-cost: 1156   maxlim: 167417620   bits: 29/28
c ---[ 491]---> Sorter-cost:14223     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> Adder-cost: 582   maxlim: 6355710   bits: 24/23
c ---[ 487]---> Adder-cost: 512   maxlim: 6290110   bits: 24/23
c ---[ 485]---> Adder-cost: 1182   maxlim: 136452120   bits: 28/28
c ---[ 483]---> Adder-cost: 978   maxlim: 167087300   bits: 28/28
c ---[ 481]---> Adder-cost: 498   maxlim: 4602657   bits: 24/23
c ---[ 479]---> Adder-cost: 1469   maxlim: 488107800   bits: 30/29
c ---[ 477]---> Sorter-cost:19809     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost:14507     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:16581     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost:15972     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> Sorter-cost:13167     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> Sorter-cost:11362     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> Adder-cost: 1638   maxlim: 357104750   bits: 30/29
c ---[ 463]---> Sorter-cost:11803     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Adder-cost: 624   maxlim: 25422784   bits: 26/25
c ---[ 459]---> Adder-cost: 1190   maxlim: 44106955   bits: 27/26
c ---[ 457]---> Sorter-cost:11882     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Adder-cost: 728   maxlim: 7928502   bits: 24/23
c ---[ 453]---> Sorter-cost:15069     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:16676     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> Adder-cost: 554   maxlim: 9452246   bits: 24/24
c ---[ 447]---> Sorter-cost:17914     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:13819     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 443]---> Sorter-cost:15298     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost:14224     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Sorter-cost:15766     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost:20649     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost:22644     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost:11292     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 431]---> Sorter-cost:14289     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost:11248     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost:11758     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost:22158     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 423]---> Adder-cost: 528   maxlim: 5905134   bits: 24/23
c ---[ 421]---> Sorter-cost:25349     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> Sorter-cost:19798     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> Sorter-cost:17602     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> Adder-cost: 1258   maxlim: 219514200   bits: 29/28
c ---[ 413]---> Adder-cost: 1126   maxlim: 118265280   bits: 28/27
c ---[ 411]---> Adder-cost: 1214   maxlim: 27641475   bits: 26/25
c ---[ 409]---> Sorter-cost:16259     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> Sorter-cost:11205     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Sorter-cost:13572     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Adder-cost: 1131   maxlim: 19981915   bits: 26/25
c ---[ 401]---> Adder-cost: 468   maxlim: 6978296   bits: 24/23
c ---[ 399]---> Adder-cost: 822   maxlim: 20933712   bits: 26/25
c ---[ 397]---> Sorter-cost:14853     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> Adder-cost: 1768   maxlim: 620820800   bits: 31/30
c ---[ 393]---> Sorter-cost:13952     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> Adder-cost: 444   maxlim: 4422283   bits: 23/23
c ---[ 389]---> Sorter-cost:13681     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 387]---> Adder-cost: 480   maxlim: 5815043   bits: 24/23
c ---[ 385]---> Sorter-cost:17190     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 383]---> Adder-cost: 338   maxlim: 5864183   bits: 23/23
c ---[ 381]---> Sorter-cost:13695     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:17359     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> Adder-cost: 640   maxlim: 25684968   bits: 26/25
c ---[ 375]---> Sorter-cost:10971     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Adder-cost: 1939   maxlim: 801030500   bits: 31/30
c ---[ 371]---> Adder-cost: 568   maxlim: 7060146   bits: 24/23
c ---[ 369]---> Sorter-cost:11569     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 367]---> Sorter-cost:16695     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Sorter-cost:14840     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> Sorter-cost:16364     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 361]---> Sorter-cost:14386     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 359]---> Sorter-cost:16453     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 357]---> Adder-cost: 1046   maxlim: 151033200   bits: 28/28
c ---[ 355]---> Sorter-cost:16231     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 353]---> Sorter-cost:14138     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 351]---> Sorter-cost:14649     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> Sorter-cost:16440     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> Sorter-cost:14219     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 345]---> Sorter-cost:18546     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> Adder-cost: 496   maxlim: 6322856   bits: 24/23
c ---[ 341]---> Adder-cost: 1738   maxlim: 557215650   bits: 31/30
c ---[ 339]---> Adder-cost: 640   maxlim: 4979440   bits: 24/23
c ---[ 337]---> Adder-cost: 566   maxlim: 6331152   bits: 24/23
c ---[ 335]---> Sorter-cost:21408     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost:15140     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 331]---> Sorter-cost:16161     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 329]---> Sorter-cost: 9351     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 327]---> Sorter-cost:13784     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 325]---> Adder-cost: 430   maxlim: 4533030   bits: 24/23
c ---[ 323]---> Adder-cost: 452   maxlim: 8305364   bits: 24/23
c ---[ 321]---> Sorter-cost:15558     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Sorter-cost:19328     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Adder-cost: 1000   maxlim: 44387430   bits: 27/26
c ---[ 315]---> Adder-cost: 1642   maxlim: 251779300   bits: 29/28
c ---[ 313]---> Sorter-cost:15384     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost:16317     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Adder-cost: 986   maxlim: 67487810   bits: 27/27
c ---[ 307]---> Sorter-cost:16806     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> Adder-cost: 1662   maxlim: 885422300   bits: 31/30
c ---[ 303]---> Adder-cost: 702   maxlim: 7846397   bits: 24/23
c ---[ 301]---> Sorter-cost:12434     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:16774     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:16427     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 295]---> Adder-cost: 1875   maxlim: 854289700   bits: 31/30
c ---[ 293]---> Sorter-cost:12970     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost:13766     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Adder-cost: 518   maxlim: 4659992   bits: 24/23
c ---[ 287]---> Sorter-cost:15200     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost:20079     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> Adder-cost: 1020   maxlim: 21989070   bits: 26/25
c ---[ 281]---> Adder-cost: 594   maxlim: 6425317   bits: 24/23
c ---[ 279]---> Adder-cost: 598   maxlim: 5323463   bits: 24/23
c ---[ 277]---> Sorter-cost:13501     Base: 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 275]---> Sorter-cost:19539     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 273]---> Adder-cost: 650   maxlim: 8698449   bits: 24/24
c ---[ 271]---> Sorter-cost:15362     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 269]---> Sorter-cost:15701     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 267]---> Sorter-cost:21023     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 265]---> Adder-cost: 1610   maxlim: 461371850   bits: 30/29
c ---[ 263]---> Sorter-cost:13836     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 261]---> Sorter-cost:13332     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 259]---> Adder-cost: 836   maxlim: 22148568   bits: 26/25
c ---[ 257]---> Sorter-cost:12902     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> Sorter-cost:15836     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Adder-cost: 1628   maxlim: 318246375   bits: 30/29
c ---[ 251]---> Sorter-cost:18086     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Adder-cost: 547   maxlim: 3807998   bits: 23/22
c ---[ 247]---> Sorter-cost:20016     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost:16049     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost:22934     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]-/oldhome/oroussel/solvers/minisat+_script: line 9:  2568 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.74 0.92 0.91 2/54 2564
Raw data (stat): 2564 (runsolver) R 2563 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783907275 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.78 0.92 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0008 s]
Raw data (loadavg): 0.81 0.92 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0011 s]
Raw data (loadavg): 0.84 0.93 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0006 s]
Raw data (loadavg): 0.87 0.93 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0035 s]
Raw data (loadavg): 0.89 0.93 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0027 s]
Raw data (loadavg): 0.90 0.93 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0033 s]
Raw data (loadavg): 0.92 0.93 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0042 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0034 s]
Raw data (loadavg): 0.94 0.94 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.95 0.94 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+799.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+809.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+819.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+829.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+839.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+849.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+859.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+869.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+879.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+889.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+899.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+909.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+919.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+929.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+939.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+949.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+959.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+969.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+979.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+989.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+999.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1149.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1209.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1219.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.78 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 2568
Raw data (stat): 2564 (minisat+_script) S 2563 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783907275 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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